Proof of Invariance of Finite Sums and Products under Reindexing by a Permutation

We prove claim 1. Claim 2 follows by the same argument with the addition of $K$ replaced by its multiplication, using claim 3 of Extraction of a Term from a Finite Sum or Product in a Field in place of claim 2 of that lemma, and claim 1 of Properties of Finite Products in place of claim 1 of Properties of Finite Sums.

We argue by induction on $n$, using the induction principle for the natural numbers with successor map $S$. Let $\mathcal{P}$ be the set of natural numbers $n$ such that the identity of claim 1 holds for every map $a:[n]\to K$ and every bijection $\sigma:[n]\to[n]$.

Base. $[1]$ consists of $1$ alone, so $\sigma(1)=1$ and both sides equal $a_{1}$ by claim 1 of Properties of Finite Sums. Hence $1\in\mathcal{P}$.

Step. Suppose $n\in\mathcal{P}$, and let $a:[S(n)]\to K$ and a bijection $\sigma:[S(n)]\to[S(n)]$ be given. Since $\sigma$ is a bijection there is exactly one $j\in[S(n)]$ with $\sigma(j)=S(n)$.

Let $b:[S(n)]\to K$ be given by $b_{k}=a_{\sigma(k)}$, and let $g_{j}:[n]\to[S(n)]$ be the gap map of Extraction of a Term from a Finite Sum or Product in a Field. Claim 2 of that lemma, applied to $b$ at the index $j$, gives

Let $E$ be the set of those $l\in[S(n)]$ with $l\ne j$, and let $D$ be the set of those $m\in[S(n)]$ with $m\ne S(n)$. By claim 1 of Extraction of a Term from a Finite Sum or Product in a Field, $g_{j}$ is a bijection from $[n]$ onto $E$. By claim 3 of Injectivity, Composition, and Restriction of Bijections the restriction of $\sigma$ to $E$ is a bijection from $E$ onto its image $\sigma(E)$; and $\sigma(E)=D$, because $\sigma$ is injective by claim 1 of Injectivity, Composition, and Restriction of Bijections with $\sigma(j)=S(n)$, so no element of $E$ is sent to $S(n)$, while every $m\in D$ is $\sigma(l)$ for some $l\in[S(n)]$ by surjectivity, and that $l$ lies in $E$ since $\sigma(j)=S(n)\ne m$. Moreover $D=[n]$: if $m\in[S(n)]$ and $m\ne S(n)$ then $m<S(n)$ and hence $m\le n$, by the order facts of Properties of the Order on the Natural Numbers; conversely $m\le n<S(n)$ for $m\in[n]$.

Therefore the map $\tau:[n]\to[n]$ given by $\tau(k)=\sigma(g_{j}(k))$ is a composite of two bijections, hence a bijection by claim 2 of Injectivity, Composition, and Restriction of Bijections.

Let $a'$ be the restriction of $a$ to $[n]$. Since $\tau(k)\in[n]$ we have $a_{\sigma(g_{j}(k))}=a'_{\tau(k)}$, so the induction hypothesis applied to $a'$ and $\tau$ gives

Finally, by claim 1 of Properties of Finite Sums, in its restriction and recursion parts,

Combining this with the previous display and with (i) gives $\sum_{k=1}^{S(n)}a_{\sigma(k)}=\sum_{k=1}^{S(n)}a_{k}$. Hence $S(n)\in\mathcal{P}$, and by induction $\mathcal{P}$ contains every natural number.