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 $\phi:|T|\to T$. Then $h\circ\phi$ enumerates $S$, and [F1] gives $\sum_{t\in T}a_{h(t)}=\sum_{k<|T|}a_{h(\phi(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 $|S|+|T|$, 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 $\phi:|S|\to S$ and $\psi:|T|\to T$. The disjoint slices $\{\phi(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 $|S|$ 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.