[proofplan]
We compare coefficients of the two formal [power series](/page/Power%20Series). The coefficient of $X^n$ in $A(X)B(X)$ is the convolution sum of the coefficient sequences of $A(X)$ and $B(X)$. On the combinatorial side, $\mathcal{C}_n$ is the disjoint union of the Cartesian products $\mathcal{A}_i\times \mathcal{B}_j$ with $i+j=n$, so its cardinality is the same convolution sum. Since all coefficients agree, the two formal power series are equal.
[/proofplan]
[step:Write the coefficient sequences for the three generating functions]
For each integer $n\geq 0$, define the integers $a_n$, $b_n$, and $c_n$ by
\begin{align*}
a_n:=|\mathcal{A}_n|.
\end{align*}
\begin{align*}
b_n:=|\mathcal{B}_n|.
\end{align*}
\begin{align*}
c_n:=|\mathcal{C}_n|.
\end{align*}
Because every graded piece of $\mathcal{A}$ and $\mathcal{B}$ is finite, $a_n,b_n\in \mathbb{Z}_{\geq 0}$ for all $n\geq 0$. The definition of $\mathcal{C}_n$ will show in the next step that each $\mathcal{C}_n$ is finite, so $c_n\in \mathbb{Z}_{\geq 0}$ as well. Thus the ordinary generating functions are
\begin{align*}
A(X)=\sum_{n=0}^{\infty}a_nX^n.
\end{align*}
\begin{align*}
B(X)=\sum_{n=0}^{\infty}b_nX^n.
\end{align*}
\begin{align*}
C(X)=\sum_{n=0}^{\infty}c_nX^n.
\end{align*}
[/step]
[step:Count the $n$th graded piece of the product class]
Fix an integer $n\geq 0$. For each pair of integers $(i,j)$ with $i,j\geq 0$ and $i+j=n$, define
\begin{align*}
D_{i,j}:=\mathcal{A}_i\times \mathcal{B}_j.
\end{align*}
Each $D_{i,j}$ is finite because it is the Cartesian product of two finite sets, and
\begin{align*}
|D_{i,j}|=|\mathcal{A}_i|\,|\mathcal{B}_j|=a_i b_j.
\end{align*}
The definition of $\mathcal{C}_n$ gives
\begin{align*}
\mathcal{C}_n=\bigcup_{\substack{i, j\geq 0, i+j=n}}D_{i,j}.
\end{align*}
This union is disjoint. Indeed, if $(a,b)\in D_{i,j}\cap D_{i',j'}$, then $a\in \mathcal{A}_i\cap \mathcal{A}_{i'}$ and $b\in \mathcal{B}_j\cap \mathcal{B}_{j'}$. Since the graded pieces of $\mathcal{A}$ are pairwise disjoint, $i=i'$, and since the graded pieces of $\mathcal{B}$ are pairwise disjoint, $j=j'$.
Therefore $\mathcal{C}_n$ is a finite disjoint union, and finite additivity of cardinality gives
\begin{align*}
c_n=|\mathcal{C}_n|=\sum_{i=0}^{n}|\mathcal{A}_i|\,|\mathcal{B}_{n-i}|=\sum_{i=0}^{n}a_i b_{n-i}.
\end{align*}
[guided]
Fix an integer $n\geq 0$. The goal is to understand exactly what objects have total grade $n$. If the first component has grade $i$, then the second component must have grade $n-i$. Thus for each $i\in\{0,\dots,n\}$, define
\begin{align*}
D_{i,n-i}:=\mathcal{A}_i\times \mathcal{B}_{n-i}.
\end{align*}
This is the set of all pairs whose first entry has grade $i$ and whose second entry has grade $n-i$.
Since $\mathcal{A}_i$ and $\mathcal{B}_{n-i}$ are finite sets, their Cartesian product is finite and has cardinality
\begin{align*}
|D_{i,n-i}|=|\mathcal{A}_i|\,|\mathcal{B}_{n-i}|=a_i b_{n-i}.
\end{align*}
The product formula for finite Cartesian products is being applied to the two finite sets $\mathcal{A}_i$ and $\mathcal{B}_{n-i}$.
Now we assemble all possible grade splits. By definition, a pair $(a,b)$ lies in $\mathcal{C}_n$ precisely when there are integers $i,j\geq 0$ with $i+j=n$, $a\in\mathcal{A}_i$, and $b\in\mathcal{B}_j$. Equivalently,
\begin{align*}
\mathcal{C}_n=\bigcup_{i=0}^{n}D_{i,n-i}.
\end{align*}
The important point is that this union is disjoint. Suppose a pair $(a,b)$ belongs to both $D_{i,n-i}$ and $D_{k,n-k}$. Then $a\in\mathcal{A}_i\cap\mathcal{A}_k$. Since the graded pieces of $\mathcal{A}$ are pairwise disjoint, this forces $i=k$. Once $i=k$, the second indices also agree because $n-i=n-k$. Hence no pair is counted twice.
Therefore $\mathcal{C}_n$ is a finite disjoint union of the sets $D_{i,n-i}$. Finite additivity of cardinality gives
\begin{align*}
|\mathcal{C}_n|=\sum_{i=0}^{n}|D_{i,n-i}|.
\end{align*}
Substituting the Cartesian-product count for each summand yields
\begin{align*}
c_n=|\mathcal{C}_n|=\sum_{i=0}^{n}|\mathcal{A}_i|\,|\mathcal{B}_{n-i}|=\sum_{i=0}^{n}a_i b_{n-i}.
\end{align*}
This is the combinatorial version of convolution: total grade $n$ is obtained by summing over all ways to split $n$ into a grade from $\mathcal{A}$ and a grade from $\mathcal{B}$.
[/guided]
[/step]
[step:Compute the coefficient of the product generating function]
For a formal power series $P(X)=\sum_{m=0}^{\infty}p_mX^m\in \mathbb{Z}[[X]]$ and an integer $n\geq 0$, let $[X^n]P(X):=p_n$ denote the coefficient of $X^n$ in $P(X)$. The ring $\mathbb{Z}$ is a commutative ring, and $A(X),B(X)\in \mathbb{Z}[[X]]$ have coefficient sequences $(a_n)_{n\geq 0}$ and $(b_n)_{n\geq 0}$. Applying [citetheorem:8150] in the ring $\mathbb{Z}$ gives, for every integer $n\geq 0$,
\begin{align*}
[X^n]\bigl(A(X)B(X)\bigr)=\sum_{i=0}^{n}a_i b_{n-i}.
\end{align*}
By the previous step, the right-hand side is $c_n$. Hence
\begin{align*}
[X^n]\bigl(A(X)B(X)\bigr)=c_n=[X^n]C(X)
\end{align*}
for every integer $n\geq 0$.
[/step]
[step:Conclude equality of the formal power series]
We have shown that
\begin{align*}
[X^n]\bigl(A(X)B(X)\bigr)=[X^n]C(X)
\end{align*}
for every integer $n\geq 0$. By [citetheorem:8148], formal power series over the commutative ring $\mathbb{Z}$ are equal if and only if all corresponding coefficients are equal. Therefore
\begin{align*}
C(X)=A(X)B(X).
\end{align*}
This is the desired product rule for ordinary generating functions of graded classes.
[/step]
