Proof of The Product of Two Sums over Finite Index Sets is a Sum over the Cartesian Product

Write $H:F\times G\to K$ for the map $H(p)=a(p_{1})\,b(p_{2})$. Since $F$ is nonempty and finite it has $r$ elements for some natural number $r$, by Number of Elements of a Set. We argue by induction on $r$, using Principle of Induction for the Natural Numbers, on the statement $P(r)$: for every set $F$ with $r$ elements, every nonempty finite set $G$ and all maps $a:F\to K$ and $b:G\to K$, the asserted identity holds.

Base case $P(1)$. Let $\chi:[1]\to F$ be a bijection and put $x_{0}=\chi(1)$; since $[1]=\{1\}$ by claim 2 of Basic Properties of Initial Segments of the Natural Numbers, every element of $F$ equals $\chi(1)$, so $F=\{x_{0}\}$. By claim 1 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set,

By claim 1 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets the map $\iota:G\to F\times G$ with $\iota(y)=(x_{0},y)$ is a bijection onto $\{x_{0}\}\times G=F\times G$. Applying claim 2 of Properties of a Sum over a Finite Index Set to $H$ and $\iota$, and then claim 4 of that lemma,

where the middle equality uses that the components of $(x_{0},y)$ are $x_{0}$ and $y$, by Characteristic Property of the Ordered Pair. This is the asserted identity.

Induction step. Assume $P(r)$ and let $F$ have $S(r)$ elements, where $S$ is the successor map of Natural Numbers. By claim 2 of Peeling an Element off a Finite Set, and Unions of Finite Sets there are a subset $F'\subseteq F$ with $r$ elements and an element $c\in F$ with $c\notin F'$ such that $F=F'\cup\{c\}$. By claim 2 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set,

so by the distributive law of the field $K$,

The hypothesis $P(r)$, applied to $F'$ and the restriction of $a$ to $F'$, identifies the first summand with $\sum_{p\in F'\times G}H(p)$. The set $\{c\}$ has $1$ element by claim 2 of Basic Properties of Finite Sets, so the base case, applied to $\{c\}$ and the restriction of $a$ to $\{c\}$, identifies the second summand with $\sum_{q\in\{c\}\times G}H(q)$.

The sets $F'\times G$ and $\{c\}\times G$ are nonempty subsets of $F\times G$; they are disjoint, because the first component of an element of $F'\times G$ lies in $F'$ while that of an element of $\{c\}\times G$ is $c\notin F'$; and their union is $F\times G$, because every $p\in F\times G$ has $p_{1}\in F=F'\cup\{c\}$. Hence claim 3 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set gives

which completes the induction step and the proof.