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

Let $K$ be a field, with additive identity $0$. Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition. The notions finite and has $k$ elements are those of the indicated definitions. Sums over a finite index set are those of Sum over a Finite Index Set; a sum $\sum_{x\in E}h(x)$ over a subset $E$ of the domain of $h$ is the sum over $E$ of the restriction of $h$ to $E$.

Then the following hold.

1. (Singleton) Let $a$ be an object and let $h:\{a\}\to K$ be a map. Then $\{a\}$ is nonempty and finite and

$$\sum_{x\in\{a\}}h(x)=h(a).$$

2. (Peeling) Let $F$ be a nonempty finite set, let $a$ be an object with $a\notin F$, and let $h:F\cup\{a\}\to K$ be a map. Then $F\cup\{a\}$ is nonempty and finite and

$$\sum_{x\in F\cup\{a\}}h(x)=\Bigl(\sum_{x\in F}h(x)\Bigr)+h(a).$$

3. (Splitting) Let $F$ be a finite set, let $F_{1}$ and $F_{2}$ be nonempty subsets of $F$ with $F=F_{1}\cup F_{2}$ and $F_{1}\cap F_{2}=\emptyset$, and let $h:F\to K$ be a map. Then

$$\sum_{x\in F}h(x)=\sum_{x\in F_{1}}h(x)+\sum_{x\in F_{2}}h(x).$$

4. (Terms vanishing outside a subset) Let $F$ be a nonempty finite set, let $E\subseteq F$ be nonempty, and let $h:F\to K$ be a map with $h(x)=0$ for every $x\in F\setminus E$. Then

$$\sum_{x\in F}h(x)=\sum_{x\in E}h(x).$$

5. (Interchange) Let $F$ and $G$ be nonempty finite sets, let $F\times G$ be their Cartesian product, and let $h:F\times G\to K$ be a map, whose value at the ordered pair $(x,y)$ is written $h(x,y)$. Then

$$\sum_{x\in F}\Bigl(\sum_{y\in G}h(x,y)\Bigr)=\sum_{y\in G}\Bigl(\sum_{x\in F}h(x,y)\Bigr).$$