Let \(N_{1}\) and \(N_{2}\) be as in the definition for \(\ell _{1}\) and \(\ell _{2}\) respectively. Then \(a_{\max (N_{1},N_{2})}=\ell _{1}\) and \(a_{\max (N_{1},N_{2})}=\ell _{2}\), so \(\ell _{1}=\ell _{2}\).

Take \(N=0\). Then all \(i\geq 0\) satisfy \(a_{i}=c\).

Let \(N_1\) witness stabilization of \((a_i)\) to \(\ell \) and \(N_2\) witness the eventual equality. Then for all \(i \geq \max (N_1, N_2)\), we have \(b_i = a_i = \ell \).

Let \(N_a\) and \(N_b\) witness the two stabilizations. For \(i \geq \max (N_a, N_b)\), we have \(a_i + b_i = \ell _a + \ell _b\).

Let \(N_a\) and \(N_b\) witness the two stabilizations. For \(i \geq \max (N_a, N_b)\), we have \(a_i \cdot b_i = \ell _a \cdot \ell _b\).

Let \(N\) witness the stabilization. For \(i \geq N\), we have \(-a_i = -\ell \).

By induction on \(|S|\), using Lemma 1.448 for the induction step.

For \(i \geq k\), we have \(s^i = s^k \cdot s^{i-k} = 0 \cdot s^{i-k} = 0\).

By extensionality (Lemma 1.86): for each \(n\), the \(n\)-th coefficient of \(\ell _1\) equals that of \(\ell _2\) by Lemma 1.445.

For each \(n\), the sequence \(([x^n]g, [x^n]g, \ldots )\) is constant and stabilizes to \([x^n]g\) by Lemma 1.446.

For each \(n \in \mathbb {N}\), the sequence \(([x^n](x^i))_{i \in \mathbb {N}}\) consists of a single \(1\) (at \(i = n\)) and \(0\)s elsewhere. For \(i \geq n+1\), \([x^n](x^i) = 0\), so the sequence stabilizes to \(0 = [x^n]0\).

Since \([x^0]g = 0\), we have \(\operatorname {ord}(g) \geq 1\), so \(\operatorname {ord}(g^d) \geq d {\gt} n\), and therefore \([x^n](g^d) = 0\).

For \(d {\gt} n\), we have \([x^n](g^d) = 0\) by Lemma 1.457, so those terms vanish from the infinite sum.

By strong induction on the coefficient index \(k\). For \(k = 0\), both inverse coefficients equal \(u^{-1}\). For \(k {\gt} 0\), the recursive formula for inverse coefficients involves only lower-degree coefficients of the inverse (handled by the IH) and coefficients of \(f\), \(g\) that agree by \(x^n\)-equivalence.

By Lemma 1.458, \([x^m](f \circ g)\) depends only on the first \(m+1\) coefficients of \(f\) and on powers \(g^d\) for \(d \leq m\). Since \(f_1 \overset {x^n}{\equiv } f_2\) gives \([x^d]f_1 = [x^d]f_2\) for \(d \leq m \leq n\), and \(g_1 \overset {x^n}{\equiv } g_2\) implies \(g_1^d \overset {x^n}{\equiv } g_2^d\) (by compatibility of \(\overset {x^n}{\equiv }\) with powers), the result follows.

We need to show that for each \(n\), the sequence \(([x^n] f_i)\) stabilizes to \([x^n](\sum _{m \in \mathbb {N}} g_m x^m) = g_n\). But this is exactly the hypothesis applied to \(n\).

Let \(n\in \mathbb {N}\). For each \(k\in \left\{ 0,1,\ldots ,n\right\} \), we pick an \(N_{k}\in \mathbb {N}\) such that all \(i\geq N_{k}\) satisfy \(\left[ x^{k}\right] f_{i}=\left[ x^{k}\right] f\) (such an \(N_{k}\) exists, since \(\lim \limits _{i\rightarrow \infty }f_{i}=f\)). Then, all integers \(i\geq \max \left\{ N_{0},N_{1},\ldots ,N_{n}\right\} \) satisfy \(f_{i}\overset {x^{n}}{\equiv }f\).

Let \(n\in \mathbb {N}\).

Addition. The \(n\)-th coefficient of \(f_i + g_i\) is \([x^n]f_i + [x^n]g_i\). Since \(([x^n]f_i)\) stabilizes to \([x^n]f\) and \(([x^n]g_i)\) stabilizes to \([x^n]g\), Lemma 1.448 shows that \(([x^n]f_i + [x^n]g_i)\) stabilizes to \([x^n]f + [x^n]g = [x^n](f+g)\).

Multiplication. The \(n\)-th coefficient of \(f_i g_i\) is \([x^n](f_i g_i) = \sum _{(a,b) \in \mathrm{antidiag}(n)} [x^a]f_i \cdot [x^b]g_i\). Each term \([x^a]f_i \cdot [x^b]g_i\) is a product of two stabilizing sequences (by Lemma 1.449), and a finite sum of stabilizing sequences stabilizes (by Lemma 1.451). Thus the sequence stabilizes to \(\sum _{(a,b)} [x^a]f \cdot [x^b]g = [x^n](fg)\).

For each \(n\), \(([x^n](-f_i)) = (-[x^n]f_i)\) stabilizes to \(-[x^n]f = [x^n](-f)\) by Lemma 1.450.

Write \(f_i - g_i = f_i + (-g_i)\) and apply Proposition 1.463 (addition) and Lemma 1.464.

Follows by induction on \(k\), using Proposition 1.463.

The \(0\)-th coefficient of \(g_i\) stabilizes to the \(0\)-th coefficient of \(g\). For sufficiently large \(i\), \([x^0]g_i = [x^0]g\). Since \([x^0]g_i\) is a unit, so is \([x^0]g\).

The invertibility of \(g\) follows from Lemma 1.467. For the limit equality, we write \(f_i / g_i = f_i \cdot g_i^{-1}\) and show that the coefficients of \(g_i^{-1}\) stabilize to those of \(g^{-1}\).

The key step is showing that the inverse coefficients stabilize. This is done by strong induction on the coefficient index \(n\).

Base case (\(n = 0\)): The \(0\)-th coefficient of \(g_i^{-1}\) is \(([x^0]g_i)^{-1}\). Since \([x^0]g_i\) stabilizes to \([x^0]g\), the inverse stabilizes as well.

Induction step (\(n {\gt} 0\)): The \(n\)-th coefficient of \(g_i^{-1}\) is determined by the recursive formula

By the induction hypothesis, each \([x^b](g_i^{-1})\) with \(b {\lt} n\) stabilizes. Combined with stabilization of \([x^a]g_i\) and \(([x^0]g_i)^{-1}\), the products and sums stabilize by Lemmas 1.449 and 1.451.

Once we know \(g_i^{-1}\) coefficientwise stabilizes to \(g^{-1}\), the result \(\lim f_i g_i^{-1} = f g^{-1}\) follows from Proposition 1.463 (multiplication).

First, \([x^0]g = 0\) since \([x^0]g_i = 0\) for all \(i\) and the \(0\)-th coefficient stabilizes.

For each \(n \in \mathbb {N}\), by Lemma 1.462 we can find \(N_f\) and \(N_g\) such that for \(i \geq \max (N_f, N_g)\), \(f_i \overset {x^n}{\equiv } f\) and \(g_i \overset {x^n}{\equiv } g\). By Proposition 1.338 (compatibility of \(x^n\)-equivalence with composition), \(f_i \circ g_i \overset {x^n}{\equiv } f \circ g\), so in particular \([x^n](f_i \circ g_i) = [x^n](f \circ g)\).

For each \(n\), \([x^n](f_i') = (n+1) \cdot [x^{n+1}]f_i\). Since \(([x^{n+1}]f_i)\) stabilizes to \([x^{n+1}]f\), multiplying by the constant \((n+1)\) preserves stabilization (by Lemma 1.449 with the constant sequence \((n+1)\)). Thus the sequence stabilizes to \((n+1) \cdot [x^{n+1}]f = [x^n](f')\).

For each coefficient index \(n\), only finitely many \(f_j\) have nonzero \(n\)-th coefficient (by summability). Let \(S\) be the finite set of such indices, and let \(N\) be the maximum element of \(S\) (or \(0\) if \(S\) is empty). For \(i \geq N+1\), the partial sum \(\sum _{j=0}^{i} [x^n]f_j\) includes all nonzero contributors, so it equals the infinite sum \(\sum _{j \in \mathbb {N}} [x^n]f_j\). Hence the \(n\)-th coefficient stabilizes.

By the multipliability condition, for each \(n\) there exists \(N\) such that for all \(j \geq N\), \(f_j \equiv 1 \pmod{x^{n+1}}\) (i.e., \([x^k]f_j = \delta _{k,0}\) for \(k \leq n\)). Once \(i\) exceeds \(N\), multiplying the partial product by \(f_{i+1}\) does not change the first \(n+1\) coefficients, since \(f_{i+1}\) acts as \(1\) on those coefficients. Hence the \(n\)-th coefficient of the partial product stabilizes to the \(n\)-th coefficient of the infinite product.

For each \(n\), once \(i \geq n\), the truncation \(\operatorname {trunc}_{i+1}(a)\) has \([x^n](\operatorname {trunc}_{i+1}(a)) = [x^n]a\) (since \(n {\lt} i + 1\)).

Summability. Fix a coefficient index \(n\). Let \(N\) be such that \([x^n](\sum _{j=0}^{i} f_j) = [x^n]\ell \) for all \(i \geq N\) (where \(\ell \) is the limit). Suppose for contradiction that \(i \geq N+1\) and \([x^n]f_i \neq 0\). Then

which gives \([x^n]f_i = 0\), a contradiction. So the set \(\{ i : [x^n]f_i \neq 0\} \subseteq \{ 0, 1, \ldots , N\} \) is finite.

Equality. Once summability is established, Theorem 1.475 gives \(\lim _{i \to \infty } \sum _{n=0}^{i} f_n = \sum _{n \in \mathbb {N}} f_n\). By uniqueness of limits, \(\sum _{n \in \mathbb {N}} f_n = \ell \).

Multipliability. We first show that \([x^0]f_i = 1\) for all \(i\). Since the \(0\)-th coefficient of \(\prod _{j=0}^{i} f_j\) stabilizes to \([x^0]\ell \), and \([x^0](\prod _{j=0}^{i} f_j) = \prod _{j=0}^{i} [x^0]f_j\), the product of the constant coefficients stabilizes; this forces \([x^0]f_i = 1\) for all sufficiently large \(i\), and since the constant coefficients are units whose product stabilizes, we get \([x^0]f_i = 1\) for all \(i\).

Next, we need to show that for each \(n\), eventually \(f_i \equiv 1 \pmod{x^{n+1}}\) (i.e., \([x^k]f_i = \delta _{k,0}\) for all \(k \leq n\)).

We prove this by strong induction on \(k\): for \(0 {\lt} k \leq n\) and sufficiently large \(i\), \([x^k]f_i = 0\).

Let \(P_i = \prod _{j=0}^{i-1} f_j\) denote the partial product (so that the partial product up to \(i\) is \(P_i \cdot f_i\)). By hypothesis, the \(k\)-th coefficient of both \(P_{i+1} = P_i \cdot f_i\) and \(P_i\) eventually stabilizes to \([x^k]\ell \). Hence eventually \([x^k](P_i \cdot f_i) = [x^k]P_i\).

Expanding \([x^k](P_i \cdot f_i)\) via the convolution formula and using \([x^0]f_i = 1\), we get

Since \([x^0]P_i = 1\) (as a product of FPSs with constant term \(1\)), the last term equals \([x^k]f_i\). By the induction hypothesis, the middle sum vanishes (since \(0 {\lt} b {\lt} k\) and \([x^b]f_i = 0\) for large \(i\)). Thus \([x^k]f_i = 0\).

Note: the formalization adds \([x^0]f_i = 1\) as an explicit hypothesis rather than deriving it from the existence of the limit.

Equality. Once multipliability is established, Theorem 1.476 gives \(\lim \prod _{n=0}^{i} f_n = \prod _{n \in \mathbb {N}} f_n\), and uniqueness of limits gives the result.