Proof of Interchange of a Finite Double Sum

Let $S$ be the successor map of Natural Numbers and write (S$k$) for claim $k$ of Properties of Finite Sums. Keeping $K$ and $n$ fixed, we induct on the length of the outer tuple.

Let $A$ be the set of those $p\in\mathbb{N}$ such that for every $a\in(K^{n})^{p}$ the tuples $b\in K^{p}$ and $c\in K^{n}$ formed from $a$ as in the statement satisfy $\sum_{j=1}^{p}b_{j}=\sum_{k=1}^{n}c_{k}$.

Base case. Let $a\in(K^{n})^{1}$. By (S1), $\sum_{j=1}^{1}b_{j}=b_{1}=\sum_{k=1}^{n}(a_{1})_{k}$, and $c_{k}=(a_{1})_{k}$ for every $k\in[n]$, so $\sum_{k=1}^{n}c_{k}=\sum_{k=1}^{n}(a_{1})_{k}$ as well. Hence $1\in A$.

Induction step. Let $p\in A$ and $a\in(K^{n})^{S(p)}$. By claims 4, 5 and 1 of Properties of the Order on the Natural Numbers we have $p\in[S(p)]$, so $a$ restricts to $a'\in(K^{n})^{p}$; let $b'\in K^{p}$ and $c'\in K^{n}$ be formed from $a'$. Since $a'_{j}=a_{j}$ for $j\in[p]$, the tuple $b'$ is the restriction of $b$ to $[p]$, and the restriction part of (S1) gives $c'_{k}=\sum_{j=1}^{p}(a_{j})_{k}$ for every $k\in[n]$.

By the recursion and restriction parts of (S1), then the induction hypothesis, then (S2),

Applying (S1) for each $k\in[n]$ to the $S(p)$-tuple with components $(a_{j})_{k}$ gives $c_{k}=c'_{k}+(a_{S(p)})_{k}$, so the right-hand side above is $\sum_{k=1}^{n}c_{k}$. Hence $S(p)\in A$.

By Principle of Induction for the Natural Numbers, $A=\mathbb{N}$; in particular $m\in A$.