Concatenation of Finite Sums

Let $K$ be a \reftext{def:field-c54-2026b}{field}. Let $\mathbb{N}$ be the set of \reftext{def:natural-numbers-2026a}{natural numbers}, with addition $+$ and successor map $S$ as in that definition, and for a natural number $p$ let $[p]$ be the \reftext{def:initial-segment-natural-numbers-2026a}{initial segment} determined by $p$, that is, the set of natural numbers $k$ with $1\le k\le p$.

Let $m,n\in\mathbb{N}$ and let $a\in K^{n+m}$ be an \reftext{def:finite-tuple-power-2026a}{$(n+m)$-tuple} in $K$, with components $a_{k}$; by that definition $a$ is a map from $[n+m]$ to $K$. Then $[n]\subseteq[n+m]$, and $n+k\in[n+m]$ for every $k\in[m]$, by claims 4 and 6 of \ref{lem:order-natural-numbers-2026a}. Let $a'\in K^{n}$ be the restriction of $a$ to $[n]$, and let $b\in K^{m}$ be the $m$-tuple with components $b_{k}=a_{n+k}$.

All sums below are \reftext{def:finite-sum-field-2026b}{finite sums in a field}. Then