Summable families of formal series are locally finite in every coefficient range

Let $(f_i{)}_{i\in I}$ be a family in $R\mathrm{⟦}x\mathrm{⟧}$. It is summable if, for every $N\in \mathbb{N}$, only finitely many $i\in I$ have a nonzero coefficient in a degree $n<N$. Its sum is defined coefficientwise by

$[x^n]{\sum }_{i\in I}{f}_i:={\sum }_{i\in I}[x^n]f_i,$

where the right side is the finite sum over indices whose displayed coefficient is nonzero. The empty family is summable and has sum $0$.

For a sequence $(u_k{)}_{k\ge 0}$ with ${\mathrm{ord}}_x(u_k)\to +\mathrm{\infty }$, define

${\prod }_{k\ge 0}(1+u_k)$

to be the unique series whose residue class modulo $x^N$ equals every sufficiently long finite partial product modulo $x^N$. Such stabilization is part of the definition until existence and uniqueness are proved. The empty product is $1$.