Most parts of Theorem 1.76 are straightforward to verify. Let us check the associativity of multiplication.

Let \(\mathbf{a},\mathbf{b},\mathbf{c}\in K\left[\left[x\right]\right]\). We must prove that \(\mathbf{a}\left(\mathbf{bc}\right) = \left( \mathbf{ab}\right)\mathbf{c}\). Let \(n\in \mathbb {N}\). Consider the two equalities

and

The right hand sides are equal since

and \(n-j-i=n-i-j\). Thus \(\left[x^{n}\right]\left(\left(\mathbf{ab}\right)\mathbf{c}\right) =\left[x^{n}\right]\left(\mathbf{a}\left(\mathbf{bc}\right)\right)\) for each \(n\in \mathbb {N}\), which entails \(\left(\mathbf{ab}\right) \mathbf{c}=\mathbf{a}\left(\mathbf{bc}\right)\).

The remaining claims of Theorem 1.76 follow by similar (and easier) coefficient-wise verifications. In the Lean formalization, the commutative ring and module structures are provided by Mathlib’s existing instances on power series.

This rewrites the antidiagonal sum from Definition 1.74 as a range sum using the bijection \((i, n-i) \leftrightarrow i \in \{ 0, \ldots , n\} \).

Let \(J\) be a subset of \(I\). We must prove that the subfamily \(\left(\mathbf{a}_{i}\right)_{i\in J}\) is summable.

Let \(n\in \mathbb {N}\). Then, all but finitely many \(i\in I\) satisfy \(\left[ x^{n}\right]\mathbf{a}_{i}=0\) (since the family \(\left(\mathbf{a}_{i}\right)_{i\in I}\) is summable). Hence, all but finitely many \(i\in J\) satisfy \(\left[x^{n}\right]\mathbf{a}_{i}=0\) (since \(J\) is a subset of \(I\)). Since we have proved this for each \(n\in \mathbb {N}\), we thus conclude that the family \(\left(\mathbf{a}_{i}\right)_{i\in J}\) is summable.

The proof is tedious (as there are many rules to check), but fairly straightforward (the idea is always to focus on a single coefficient, and then to reduce the infinite sums to finite sums). For example, consider the discrete Fubini rule, which says that

whenever \(\left(\mathbf{a}_{i,j}\right)_{\left(i,j\right) \in I\times J}\) is a summable family of FPSs. In order to prove this rule, we fix a summable family \(\left(\mathbf{a}_{i,j}\right)_{\left(i,j\right) \in I\times J}\) of FPSs. It is easy to see that the families \(\left( \mathbf{a}_{i,j}\right)_{j\in J}\) for all \(i\in I\) are summable as well, as are the families \(\left(\mathbf{a}_{i,j}\right)_{i\in I}\) for all \(j\in J\), and the families \(\left(\sum _{j\in J}\mathbf{a}_{i,j}\right)_{i\in I}\) and \(\left(\sum _{i\in I}\mathbf{a}_{i,j}\right)_{j\in J}\).

To verify the Fubini identity, it suffices to check that

for each \(n\in \mathbb {N}\). Fix \(n\in \mathbb {N}\); then, we have \(\left[ x^{n}\right]\left(\mathbf{a}_{i,j}\right) =0\) for all but finitely many \(\left(i,j\right) \in I\times J\) (since the family \(\left(\mathbf{a}_{i,j}\right)_{\left(i,j\right) \in I\times J}\) is summable). That is, the set of all pairs \(\left(i,j\right) \in I\times J\) satisfying \(\left[ x^{n}\right]\left(\mathbf{a}_{i,j}\right) \neq 0\) is finite. Hence, the set \(I^{\prime }\) of the first entries and the set \(J^{\prime }\) of the second entries of all these pairs are also finite. The three sums reduce to finite sums over \(I^{\prime }\times J^{\prime }\), which are equal by the usual Fubini rule for finite sums. See [ 19s , proof of Proposition 7.2.11 ] for more details.

If \(n\) is a positive integer, then

A similar argument for \(n=0\) yields \(\left[x^{0}\right]\left(x\cdot \mathbf{a}\right)=0\). Thus, for each \(n\in \mathbb {N}\),

In other words, \(x\cdot \mathbf{a}=\left(0,a_{0},a_{1},a_{2},\ldots \right)\).

We induct on \(k\).

Induction base: We have \(x^{0}=\underline{1}=\left(1,0,0,0,0,\ldots \right) = \left(\underbrace{0,0,\ldots ,0}_{0\text{ times}},1,0,0,0,\ldots \right)\).

Induction step: Let \(m\in \mathbb {N}\). Assume that Proposition 1.84 holds for \(k=m\). We have \(x^{m}=\left(\underbrace{0,0,\ldots ,0}_{m\text{ times}},1,0,0,0,\ldots \right)\). Thus, Lemma 1.83 (applied to \(\mathbf{a}=x^{m}\)) yields

Since \(x\cdot x^{m}=x^{m+1}\), this completes the induction step.

By Proposition 1.84, we have

Immediate from the definition of FPS as a sequence.

Follows from the product formula with \(n=0\): \(\left[x^{0}\right](\mathbf{ab}) = \sum _{i=0}^{0} \left[x^{i}\right]\mathbf{a}\cdot \left[x^{0-i}\right]\mathbf{b} = \left[x^{0}\right]\mathbf{a}\cdot \left[x^{0}\right]\mathbf{b}\).

By induction on \(k\), using Lemma 1.83 for the induction step.

For each \(n\in \mathbb {N}\), \(\{ i \mid \left[x^{n}\right](\mathbf{a}_{i}+\mathbf{b}_{i})\neq 0\} \subseteq \{ i \mid \left[x^{n}\right]\mathbf{a}_{i}\neq 0\} \cup \{ i \mid \left[x^{n}\right]\mathbf{b}_{i}\neq 0\} \), and the union of two finite sets is finite.

For each \(n\), \(\left[x^{n}\right](-\mathbf{a}_{i})=-\left[x^{n}\right]\mathbf{a}_{i}\), so \(\{ i \mid \left[x^{n}\right](-\mathbf{a}_{i})\neq 0\} = \{ i \mid \left[x^{n}\right]\mathbf{a}_{i}\neq 0\} \).

\(\{ i \mid a_{i}+b_{i}\neq 0\} \subseteq \{ i \mid a_{i}\neq 0\} \cup \{ i \mid b_{i}\neq 0\} \), and the union of two finite sets is finite.

\(\{ i \mid -a_{i}\neq 0\} =\{ i \mid a_{i}\neq 0\} \).

Write \(a_i - b_i = a_i + (-b_i)\) and apply Lemma 1.91 and Lemma 1.92.

All three sums can be computed over the finite set \(S = \{ i \mid a_i\neq 0\} \cup \{ i \mid b_i\neq 0\} \), so this reduces to the finite sum identity \(\sum _{i\in S}(a_i+b_i)=\sum _{i\in S}a_i+\sum _{i\in S}b_i\).

The support of \((c\, a_i)\) is contained in the support of \((a_i)\), so this reduces to the finite identity \(\sum _{i\in S}c\, a_i = c\sum _{i\in S}a_i\).

Write \(\mathbf{a}_i - \mathbf{b}_i = \mathbf{a}_i + (-\mathbf{b}_i)\) and apply Lemma 1.89 and Lemma 1.90.

For each \(n\), \(\{ i \mid [x^n]\mathbf{a}_i \neq 0\} \subseteq \{ i \mid \mathbf{a}_i \neq 0\} \), which is finite by hypothesis.

Follows from \([x^n]x^k = \delta _{n,k}\) (Proposition 1.84) and \([x^n](\underline{a}\cdot f) = a\cdot [x^n]f\).

By commutativity of multiplication, \(\mathbf{a}\cdot x = x\cdot \mathbf{a}\), so this follows from Lemma 1.83.

By commutativity: \(\mathbf{a}\cdot x^k = x^k\cdot \mathbf{a}\), so this follows from Lemma 1.88.

Immediate from the definitions.

Multiply out the identity \(\left(1+x\right)^{a+b}=\left(1+x\right)^{a}\left(1+x\right)^{b}\) using the binomial formula and compare the coefficient of \(x^{n}\) on both sides. The left side gives \(\binom {a+b}{n}\), and the right side gives \(\sum _{k=0}^{n}\binom {a}{k}\binom {b}{n-k}\) by the product formula for FPSs.

Rewrites the antidiagonal sum from Proposition 1.104 as a range sum.

Fix \(n\in \mathbb {N}\) and \(b\in \mathbb {N}\). By Proposition 1.104, the equality

holds for each \(a\in \mathbb {N}\). However, both sides are polynomials in \(a\):

Two univariate polynomials that agree on all of \(\mathbb {N}\) (infinitely many points) must be identical. Hence the equality holds for all \(a\in \mathbb {C}\).

Now fix \(a\in \mathbb {C}\) and repeat the argument with \(b\) as the variable: both sides are polynomials in \(b\) that agree on \(\mathbb {N}\), hence they agree on \(\mathbb {C}\). (See [ 20f , proofs of Lemma 7.5.8 and Theorem 7.5.3 ] or [ 19s , § 2.17.3 ] for this proof in more detail. Alternatively, see [ Grinbe15 , § 3.3.2 and § 3.3.3 ] for two other proofs.)