Proof of Peeling, Splitting, and Interchange for Sums over a Finite Index Set

Throughout, enumerations of a finite set are the bijections supplied by Number of Elements of a Set, sums with a numerical index range are the finite sums of $K$, and a sum over a finite index set is evaluated through Sum over a Finite Index Set, whose value does not depend on the enumeration chosen.

Claim 1. By claim 2 of Basic Properties of Finite Sets the set $\{a\}$ has $1$ element, so it is nonempty and finite. By claim 2 of Basic Properties of Initial Segments of the Natural Numbers we have $[1]=\{1\}$, and the map $\varphi:[1]\to\{a\}$ with $\varphi(1)=a$ is a bijection. Hence, by Sum over a Finite Index Set and the identity $\sum_{k=1}^{1}c_{k}=c_{1}$ of claim 1 of Properties of Finite Sums,

Claim 2. Let $k$ be the number of elements of $F$ and let $\psi:[k]\to F$ be a bijection. By claim 2 of Basic Properties of Finite Sets the set $F\cup\{a\}$ has $S(k)$ elements, so it is nonempty and finite. By claim 3 of Basic Properties of Initial Segments of the Natural Numbers we have $S(k)\notin[k]$ and $[S(k)]=[k]\cup\{S(k)\}$, so the prescription

defines a map $\varphi:[S(k)]\to F\cup\{a\}$. It is a bijection: an element $y\in F$ satisfies $y\ne a$, and $\varphi(j)=y$ holds exactly for the unique $j\in[k]$ with $\psi(j)=y$; and since $\varphi(j)\in F$ for $j\in[k]$, the equality $\varphi(j)=a$ holds exactly for $j=S(k)$.

Let $c:[S(k)]\to K$ be the map with $c_{j}=h(\varphi(j))$; its restriction to $[k]$ is the map $j\mapsto h(\psi(j))$. By claim 1 of Properties of Finite Sums, first in its restriction form and then in its recursion form,

By Sum over a Finite Index Set, evaluated with the enumeration $\varphi$ on the left and with $\psi$ on the right, this is the asserted identity.

Claim 3. The set $F_{2}$ is a subset of the finite set $F$, hence finite by claim 3 of Basic Properties of Finite Sets, and it is nonempty, so it has $m$ elements for some $m\in\mathbb{N}$. We argue by induction on $m$, using Principle of Induction for the Natural Numbers, on the statement $P(m)$: for every finite set $F$, all nonempty subsets $F_{1},F_{2}\subseteq F$ with $F=F_{1}\cup F_{2}$, $F_{1}\cap F_{2}=\emptyset$ and $F_{2}$ having $m$ elements, and every map $h:F\to K$, the asserted identity holds.

For $P(1)$, let $\chi:[1]\to F_{2}$ be a bijection and put $a=\chi(1)$. Since $[1]=\{1\}$ by claim 2 of Basic Properties of Initial Segments of the Natural Numbers, every element of $F_{2}$ is $\chi(1)$, so $F_{2}=\{a\}$. Disjointness gives $a\notin F_{1}$, and $F=F_{1}\cup\{a\}$. Claims 2 and 1 now give

Assume $P(m)$ and let $F_{2}$ have $S(m)$ elements. By claim 2 of Peeling an Element off a Finite Set, and Unions of Finite Sets there are a subset $D\subseteq F_{2}$ with $m$ elements and an element $a\in F_{2}$ with $a\notin D$ such that $F_{2}=D\cup\{a\}$. Put $F'=F_{1}\cup D$. Then $F'\subseteq F$ is finite by claim 3 of Basic Properties of Finite Sets; the sets $F_{1}$ and $D$ are nonempty, disjoint (both are subsets of $F_{1}$ and $F_{2}$ respectively) and have union $F'$; moreover $a\notin F'$ and $F=F'\cup\{a\}$. Claim 2 applied to $F=F'\cup\{a\}$, the hypothesis $P(m)$ applied to $F'$, and claim 2 applied to $F_{2}=D\cup\{a\}$ give

Combining them with the associativity and commutativity of addition in the field $K$ yields $P(S(m))$.

Claim 4. If $E=F$ there is nothing to prove. Otherwise $F\setminus E$ is nonempty, and $E$ and $F\setminus E$ are nonempty disjoint subsets of $F$ with union $F$, so claim 3 gives

The restriction of $h$ to $F\setminus E$ is the map $x\mapsto 0$, which coincides with the map $x\mapsto 0\,h(x)$ by Zero Products and Elementary Identities in a Field. Hence, by claim 4 of Properties of a Sum over a Finite Index Set and Zero Products and Elementary Identities in a Field again,

and adding $0$ leaves the first summand unchanged.

Claim 5. Let $r$ and $s$ be the numbers of elements of $F$ and of $G$, and let $\varphi:[r]\to F$ and $\psi:[s]\to G$ be bijections. By Sum over a Finite Index Set, for each $x\in F$,

and applying the definition once more to the sum over $F$,

Interchanging the roles of $F$ and $G$ in the same computation gives

The two right-hand sides are equal by Interchange of a Finite Double Sum, applied to the $r$-tuple of $s$-tuples $a$ with $(a_{j})_{l}=h(\varphi(j),\psi(l))$.