The category of graded $\mathbb S$-modules form a monoidal category I am reading paragraph 6.2 in Algebraic Operads by Jean-Louis Loday and Bruno Vallette. Proposition 6.2.2 states:

The category of graded $\mathbb S$-modules, with
the (composite) product $\circ$ and the unit $I=(0,\mathbb K,0,0,\dots),$ form a monoidal category denoted $\textsf{gr }\mathbb S\textsf{-Mod}.$

There is no proof in the book. Do you know where can one find it? Thanks in advance!
 A: Here is how I personally convinced myself that this is true; it may or may not be satisfying to you, but I think it is the "right way" to think about the composition product. In particular we will be able to realize it as composition on the nose, and as a byproduct we automatically construct the monad associated to an operad. This is similar to but more general than the discussion on the nLab.
Let $S = \bigsqcup_n BS_n$ be the category of finite sets and bijections. Equipped with disjoint union, this category is the free symmetric monoidal category on a point. If $R$ is any commutative ring, the presheaf category $\widehat{S} \cong [S^{op}, \text{Mod}(R)]$ (the category of "right $S$-modules in $\text{Mod}(R)$") is then the free cocomplete $\text{Mod}(R)$-enriched category on $S$; combining the two universal properties, we conclude that:

$\widehat{S}$ is the free symmetric monoidal cocomplete $\text{Mod}(R)$-enriched category on a point.

In the definition of "symmetric monoidal cocomplete" we need to require that the monoidal product distribute over colimits. This universal property says the following: if $C$ is any other symmetric monoidal cocomplete $\text{Mod}(R)$-enriched category (such as $\text{Mod}(R)$ itself, or more generally $\text{Mod}(S)$ where $S$ is a commutative $R$-algebra), which we will call a "(commutative) $\text{Mod}(R)$-algebra" for short, and $X \in C$ is an object, we get a canonical symmetric monoidal cocontinuous functor
$$\widehat{S} \ni F(n) \mapsto \bigoplus_n F(n) \otimes_{S_n} X^{\otimes n} \in C$$
where $\otimes_{S_n}$ means to take the quotient of the copower $F(n) \otimes X^{\otimes n}$ by a suitable diagonal action of $S_n$. This is, if you like, the "formal power series" or "exponential generating function" associated to an $S$-module, and the idea of the composition product is that it is "composition of formal power series." This can be made precise as follows: the existence of these universal maps associated to each $X \in C$ produces, for each $\text{Mod}(R)$-algebra $C$, a natural action of $\widehat{S}$ on $C$, given by
$$\widehat{S} \times C \ni (F, X) \mapsto \bigoplus_n F(n) \otimes_{S_n} X^{\otimes n} \in C.$$
So, $S$-modules canonically act by endofunctors on any $\text{Mod}(R)$-algebra $C$. But more is true: this action is natural in $C$, and it is universal with respect to this property:

$\widehat{S}$ is exactly the category of natural endofunctors on $\text{Mod}(R)$-algebras.

This says, formally, that $\widehat{S}$ is the category of endomorphisms of the forgetful functor from $\text{Mod}(R)$-algebras to categories. This can be proven using the fact that $\widehat{S}$ itself, by its universal property, represents this forgetful functor, which allows us to identify (by the Yoneda lemma) the above category of endofunctors with the category of endofunctors of $\widehat{S}$ itself as a $\text{Mod}(R)$-algebra, which (by a second application of the universal property) can be identified with $\widehat{S}$ itself. This gives:

$\widehat{S}$ is exactly the category of endomorphisms of $\widehat{S}$ as a $\text{Mod}(R)$-algebra.

But any such category of endomorphisms has a monoidal structure given by composition of endomorphisms! And this is exactly the composition / substitution product. As a byproduct, we immediately obtain that the category of monoids in $\widehat{S}$ with respect to the composition product is exactly the category of natural monads on $\text{Mod}(R)$-algebras; this tells us that an operad in $\widehat{S}$ is exactly a natural collection of monads on each $\text{Mod}(R)$-algebra $C$, whose underlying functor is defined by the same "formal power series" as above.
This argument may seem complicated but it is really just a mild categorification of a formally very similar but simpler argument you can apply to, say, the category of commutative $R$-algebras where $R$ is a commutative ring. Here the analogue of $\widehat{S}$ is the polynomial algebra $R[x]$ in one variable, and the argument is that $R[x]$ is 1) the set of "natural endofunctions" of a commutative $R$-algebra, and 2) that it can be identified with the set of commutative $R$-algebra morphisms $R[x] \to R[x]$ itself, which equips it with a new product, namely composition of polynomials.
