Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule

For clause 1, choose an enumeration $\varphi :\mathrm{\mid }T\mathrm{\mid }\to T$. Then $h\circ \varphi$ enumerates $S$, and [F1] gives ${\sum }_{t\in T}{a}_{h(t)}={\sum }_{k<\mathrm{\mid }T\mathrm{\mid }}{a}_{h(\varphi (k))}={\sum }_{s\in S}{a}_s$.

For clause 2, choose enumerations of $S$ and $T$ and concatenate them. By [L2] this gives an enumeration of $S\cup T$ of length $\mathrm{\mid }S\mathrm{\mid }+\mathrm{\mid }T\mathrm{\mid }$, and the splitting law in [L1] turns the resulting finite sum into the sum over $S$ followed by the sum over $T$.

For clause 3, choose enumerations $\varphi :\mathrm{\mid }S\mathrm{\mid }\to S$ and $\psi :\mathrm{\mid }T\mathrm{\mid }\to T$. The disjoint slices $\{\varphi (i)\}\times T$ cover $S\times T$; concatenate their $\psi$-enumerations in the order of $i$. By [L2] and [L3] this is an enumeration of $S\times T$, and regrouping it into the $\mathrm{\mid }S\mathrm{\mid }$ consecutive slices gives ${\sum }_{(s,t)\in S\times T}{a}_{s,t}={\sum }_{s\in S}({\sum }_{t\in T}{a}_{s,t})$.

The column-major list also enumerates $S\times T$, and permutation invariance followed by regrouping into columns gives ${\sum }_{(s,t)\in S\times T}{a}_{s,t}={\sum }_{t\in T}({\sum }_{s\in S}{a}_{s,t})$.

Steps 1.1, 1.2, 1.3 and 2.1 prove reindexing, disjoint splitting and both finite Fubini equalities.