Laws of finite sums and finite products

Base case $n=0$: every claim holds at $n=0$, since both sides of claim 1 are $0=0+0$, both sides of claim 2 are $0=\lambda \cdot 0$ and $0=\iota (0)\lambda$, claim 4 reads $0\le 0$ with no term to bound and the hypothesis ${\sum }_{k<0}{a}_k=0$ giving nothing to prove, claim 5 reads $0=c_0-c_0$, and claim 6 reads $1=1\cdot 1$ with $1>0$.

Inductive hypothesis: fix $n\in \mathbb{N}$ and assume claims 1, 2, 4, 5 and 6 hold for this $n$ and for all sequences $a,b,c$ and all $\lambda$.

Splitting, claim 3, by a separate induction on the number of trailing terms $d=n-m$ with $m$ fixed: for $d=0$ the claim reads ${\sum }_{k<m}{a}_k={\sum }_{k<m}{a}_k+0$ and ${\prod }_{k<m}{a}_k=\left({\prod }_{k<m}{a}_k\right)\cdot 1$, which hold; and if ${\sum }_{k<m+d}{a}_k={\sum }_{k<m}{a}_k+{\sum }_{j<d}{a}_{m+j}$, then ${\sum }_{k<m+d+1}{a}_k={\sum }_{k<m+d}{a}_k+a_{m+d}={\sum }_{k<m}{a}_k+({\sum }_{j<d}{a}_{m+j}+a_{m+d})={\sum }_{k<m}{a}_k+{\sum }_{j<d+1}{a}_{m+j}$ by associativity, and identically for products with $1$ in place of $0$ and multiplication in place of addition, so induction on $d$ gives claim 3 for every $m\le n$.

Additivity at $n+1$: ${\sum }_{k<n+1}(a_k+b_k)={\sum }_{k<n}(a_k+b_k)+(a_n+b_n)=({\sum }_{k<n}{a}_k+{\sum }_{k<n}{b}_k)+(a_n+b_n)=({\sum }_{k<n}{a}_k+a_n)+({\sum }_{k<n}{b}_k+b_n)={\sum }_{k<n+1}{a}_k+{\sum }_{k<n+1}{b}_k$, using the recursion clause, the hypothesis, and commutativity with associativity of addition.

Scaling at $n+1$: ${\sum }_{k<n+1}\lambda a_k={\sum }_{k<n}\lambda a_k+\lambda a_n=\lambda {\sum }_{k<n}{a}_k+\lambda a_n=\lambda ({\sum }_{k<n}{a}_k+a_n)=\lambda {\sum }_{k<n+1}{a}_k$ by the recursion clause, the hypothesis and distributivity; taking $a_k=1$ for all $k$ gives ${\sum }_{k<n+1}\lambda ={\sum }_{k<n}\lambda +\lambda =\iota (n)\lambda +\lambda =(\iota (n)+1)\lambda =\iota (n+1)\lambda$.

Monotonicity at $n+1$: assume $a_k\le b_k$ for all $k<n+1$; then $a_k\le b_k$ for all $k<n$, so the hypothesis gives ${\sum }_{k<n}{a}_k\le {\sum }_{k<n}{b}_k$, and adding the inequality $a_n\le b_n$ gives ${\sum }_{k<n+1}{a}_k={\sum }_{k<n}{a}_k+a_n\le {\sum }_{k<n}{b}_k+b_n={\sum }_{k<n+1}{b}_k$.

Telescoping at $n+1$: ${\sum }_{k<n+1}(c_{k+1}-c_k)={\sum }_{k<n}(c_{k+1}-c_k)+(c_{n+1}-c_n)=(c_n-c_0)+(c_{n+1}-c_n)=c_{n+1}-c_0$, by the recursion clause, the hypothesis and the field identities.

Products at $n+1$: ${\prod }_{k<n+1}(a_k{b}_k)=({\prod }_{k<n}(a_k{b}_k))(a_n{b}_n)=\left({\prod }_{k<n}{a}_k\right)\left({\prod }_{k<n}{b}_k\right)(a_n{b}_n)=\left({\prod }_{k<n+1}{a}_k\right)\left({\prod }_{k<n+1}{b}_k\right)$ by the recursion clause, the hypothesis, and commutativity with associativity of multiplication; and if every $a_k\ge 0$ for $k<n+1$ then ${\prod }_{k<n+1}{a}_k=\left({\prod }_{k<n}{a}_k\right)a_n$ is a product of two nonnegatives, hence nonnegative, with the same argument giving positivity from positivity since ${\prod }_{k<0}{a}_k=1>0$.

Consequences of monotonicity, completing claim 4: monotonicity itself holds at every $n$, by the induction principle applied to the base case of step 1.1 and the successor step 2.3, so it is available for an arbitrary $n$ in what follows; if $a_k\ge 0$ for all $k<n$ then comparing with the zero sequence gives ${\sum }_{k<n}{a}_k\ge {\sum }_{k<n}0=0$; for $j<n$ splitting at $j$ and then at $j+1$ writes ${\sum }_{k<n}{a}_k={\sum }_{k<j}{a}_k+a_j+{\sum }_{k=j+1}^{n-1}{a}_k$ with the first and third summands $\ge 0$, so $a_j\le {\sum }_{k<n}{a}_k$; and if moreover ${\sum }_{k<n}{a}_k=0$ then $0\le a_j\le 0$ for every $j<n$, so $a_j=0$.

By the induction principle claims 1, 2, 4, 5 and 6 hold for every $n\in \mathbb{N}$, and claim 3 was proved in step 1.3 with its consequences in step 3.1, so all six laws hold.