Proof of Splitting a Finite Sum at an Index

We argue by Principle of Induction for the Natural Numbers, with $m$ fixed, on the statement $P(n)$: for every $a:[m+n]\to K$ the displayed identity holds. Throughout, claim 1 of Properties of Finite Sums is used in both of its forms, namely that the value of a finite sum is unchanged when the family of summands is replaced by any family agreeing with it on the relevant initial segment (restriction), and that

(recursion).

Base case $n=1$. Let $a:[m+1]\to K$. By claim 1 of Arithmetic of Addition on the Natural Numbers we have $m+1=S(m)$, so recursion gives

The family $a'$ agrees with $a$ on $[m]$, so by restriction $\sum_{k=1}^{m}a_k=\sum_{k=1}^{m}a'_k$. Moreover $[1]=\{1\}$ by claim 4 of Properties of the Order on the Natural Numbers, and by recursion $\sum_{j=1}^{1}a''_j=a''_1=a_{m+1}=a_{S(m)}$. Combining the three displays gives $P(1)$.

Induction step. Assume $P(n)$ and let $a:[m+S(n)]\to K$. By identity 2 of Natural Numbers we have $m+S(n)=S(m+n)$, so recursion gives

Let $b:[m+n]\to K$ be the restriction of $a$ to $[m+n]$; this is legitimate because $m+n<m+S(n)$ by claim 6 of Properties of the Order on the Natural Numbers. By restriction, the first sum on the right is the finite sum of $b$, and $P(n)$ applied to $b$ gives

Here $b'$ is the restriction of $b$ to $[m]$, which is the restriction $a'$ of $a$ to $[m]$; and for $j\in[n]$ we have $b''_j=b_{m+j}=a_{m+j}=a''_j$, so by restriction $\sum_{j=1}^{n}b''_j=\sum_{j=1}^{n}a''_j$, where on the right $a''$ denotes the family associated with $a$ on $[S(n)]$, restricted to $[n]$.

Finally $a_{S(m+n)}=a_{m+S(n)}=a''_{S(n)}$ by the definition of $a''$, and recursion applied to $a''$ gives

Substituting and using associativity of addition in the field $K$,

which is $P(S(n))$.

By the principle of induction, $P(n)$ holds for every $n\in\mathbb{N}$.