Proof of Expanding a Product of Sums over a Fixed Finite Index Set

Each result cited is universally quantified over the data in its own statement. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, the elements of $B^{A}$ are exactly the maps $A\to B$.

Clause maps. Both maps are given by expressions and by operations over the finite sets $B$ and $A$, as in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices §maps.

Clause expansion. Let $(C_{x})_{x\in A}$ be the constant family of finite sets with $C_{x}=B$ for every $x\in A$. By Indexed Families of Sets and Their Union, Intersection and Product §union, its union $U=\bigcup_{z\in A}C_{z}$ satisfies $U\subseteq B$ and $C_{x}\subseteq U$ for every $x\in A$. Let $T=\{(x,y)\in A\times U:y\in C_{x}\}$ and let $P$ be the set of maps $\varphi:A\to U$ with $\varphi(x)\in C_{x}$ for every $x\in A$, as in Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §distributivity with $(C_{x})_{x\in A}$ in place of $(B_{x})_{x\in A}$. Since $C_{x}=B$ and $C_{x}\subseteq U\subseteq B$ for every $x\in A$, a pair $(x,y)$ lies in $T$ if and only if $x\in A$ and $y\in B$, and a map with domain $A$ lies in $P$ if and only if all its values lie in $B$. Hence $T=A\times B$ and $P=B^{A}$ by Axiom of Extensionality for Classes, and $u$ is a map $T\to R$. As $\sum_{y\in C_{x}}u(x,y)=\sum_{y\in B}u(x,y)$ for every $x\in A$, Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §distributivity for $R$, $A$, $(C_{x})_{x\in A}$ and $u$ reads

$$\prod_{x\in A}\sum_{y\in B}u(x,y)=\sum_{\varphi\in B^{A}}\prod_{x\in A}u(x,\varphi(x)),$$

the term maps on both sides being those of clause maps. This is clause expansion.