Proof of Generalized Distributivity: Expanding a Product of Finite Sums

Fix $m$ and argue by induction on $n$, using Principle of Induction for the Natural Numbers, on the statement $P(n)$: for every $n$-tuple $c$ of $m$-tuples in $K$ the asserted identity holds.

Base case $P(1)$. By claim 1 of Properties of Finite Products a product with a single factor equals that factor, so the left-hand side is $\sum_{k=1}^{m}c_{1k}$.

For the right-hand side, let $\beta:[m]\to[m]^{1}$ send $k$ to the $1$-tuple $f_{k}$ with $f_{k}(1)=k$. Since $[1]=\{1\}$ by claim 2 of Basic Properties of Initial Segments of the Natural Numbers, a map $f:[1]\to[m]$ is determined by its value at $1$, so $f=f_{f(1)}$ for every $f\in[m]^{1}$, and $f_{k}=f_{k'}$ forces $k=k'$; hence $\beta$ is a bijection. Using claim 1 of Properties of Finite Products once more, then claim 2 and claim 1 of Properties of a Sum over a Finite Index Set,

Induction step. Assume $P(n)$ and let $c$ be an $S(n)$-tuple of $m$-tuples in $K$. By the recursion in claim 1 of Properties of Finite Products,

The restriction statement in that same claim shows that products of the form $\prod_{i=1}^{n}(\cdot)$ are unchanged when the $S(n)$-tuple $c$ is replaced by the $n$-tuple of its first $n$ entries, so the hypothesis $P(n)$ applies to the first factor and gives

By claim 1 of Properties of a Sum over a Finite Index Set the second factor equals $\sum_{k\in[m]}c_{S(n)\,k}$. Both $[m]^{n}$ and $[m]$ are nonempty finite sets, by claim 3 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets and claim 1 of Basic Properties of Finite Sets, so The Product of Two Sums over Finite Index Sets is a Sum over the Cartesian Product applies and yields

where $p_{1}\in[m]^{n}$ and $p_{2}\in[m]$ are the components of $p$.

By claim 2 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets there is a bijection $q:[m]^{n}\times[m]\to[m]^{S(n)}$ such that, for every $p$, the tuple $g=q(p)$ satisfies $g(i)=p_{1}(i)$ for $i\in[n]$ and $g(S(n))=p_{2}$. For such $g$, claim 1 of Properties of Finite Products, again in its restriction and recursion forms, gives

so the summand at $p$ is the value at $q(p)$ of the map $g\mapsto\prod_{i=1}^{S(n)}c_{i\,g(i)}$ on $[m]^{S(n)}$. Reindexing along $q$ by claim 2 of Properties of a Sum over a Finite Index Set therefore gives

which is $P(S(n))$.