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

Let $K$ be a field, let $F$ and $G$ be nonempty finite sets, and let $a:F\to K$ and $b:G\to K$ be maps. Let $F\times G$ be the Cartesian product of $F$ and $G$, formed with the ordered pair; it is nonempty, and it is finite by claim 1 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets. For $p\in F\times G$ write $p_{1}\in F$ and $p_{2}\in G$ for the unique elements with $p=(p_{1},p_{2})$, unique by Characteristic Property of the Ordered Pair. Sums over a finite index set are those of Sum over a Finite Index Set.

Then