Expanding a Product of Sums over a Fixed Finite Index Set

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $R$, with $+$, $\cdot$, $0$ and $1$, be a commutative ring, let $A$ and $B$ be finite sets, and let $u:A\times B\to R$. The set $B^{A}$ of maps from $A$ to $B$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §maps.

¶ There are a map $A\to R$, $x\mapsto\sum_{y\in B}u(x,y)$, and a map $B^{A}\to R$, $\varphi\mapsto\prod_{x\in A}u(x,\varphi(x))$.

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