Splitting a Finite Sum at an Index

Let $K$ be a field, let $\mathbb{N}$ be the set of natural numbers, ordered by the relations of Order on the Natural Numbers, and for $p\in\mathbb{N}$ let $[p]$ be the initial segment determined by $p$, that is, the set of $k\in\mathbb{N}$ with $k\le p$. Sums below are the finite sums of that definition.

Let $m,n\in\mathbb{N}$ and let $a:[m+n]\to K$, with values written $a_k$.

By claim 6 of Properties of the Order on the Natural Numbers we have $m<m+n$ and $m+j\le m+n$ for every $j\in[n]$, so, using transitivity from claim 1 of that lemma, $[m]\subseteq[m+n]$ and $m+j\in[m+n]$ for every $j\in[n]$. Let $a':[m]\to K$ be the restriction of $a$ to $[m]$, and let $a'':[n]\to K$ be given by

$$a''_j=a_{m+j}\qquad (j\in[n]).$$

Then

$$\sum_{k=1}^{m+n}a_k=\sum_{k=1}^{m}a'_k+\sum_{j=1}^{n}a''_j .$$