Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either

Splitting law, base $n = 0$: the left side is $\prod_{i<m+0} g_i = \prod_{i<m} g_i$, and the right side is $\bigl(\prod_{i<m} g_i\bigr) \cdot \prod_{j<0} g_{m+j} = \bigl(\prod_{i<m} g_i\bigr) \cdot e = \prod_{i<m} g_i$; so the two agree, for every $m$.

Splitting law, inductive hypothesis: fix $n$ and assume $\prod_{i<m+n} g_i = \bigl(\prod_{i<m} g_i\bigr) \cdot \bigl(\prod_{j<n} g_{m+j}\bigr)$ for every $m$ and every family $g$.

Write $u_j := g_{m+j}$, a family $\mathbb{N} \to M$, so that $\prod_{j<n} g_{m+j} = \prod_{j<n} u_j$ and $u_n = g_{m+n}$.

In claim 2 the natural $c_j$ exists because $s_j \le s_{\sigma(j)}$, and it is unique by cancellation, so $B_j$ is well defined for every $j$ and $B : \mathbb{N} \to M$ is a family.

Regrouping law, base $r = 0$: the left side is $\prod_{j<0} B_j = e$ and the right side is $\prod_{i<s_0} g_i = \prod_{i<0} g_i = e$.

Regrouping law, inductive hypothesis: assume $\prod_{j<r} B_j = \prod_{i<s_r} g_i$ for this $r$.

Commutative case, base $n = 0$: both products are empty, hence both equal $e$.

Commutative case, inductive hypothesis: fix $n$ and assume that for every family $g$, every $\pi \in \operatorname{Sym}(n)$ and every family $h$ with $h_i = g_{\pi(i)}$ for $i<n$, one has $\prod_{i<n} h_i = \prod_{i<n} g_i$.

Successor step, the data. Let $\pi \in \operatorname{Sym}(\sigma(n))$ and let $h$ satisfy $h_i = g_{\pi(i)}$ for every $i < \sigma(n)$. Put $k := \pi^{-1}(n)$, so $k < \sigma(n)$, that is $k \le n$, and let $r$ be the natural with $k + r = n$; then $k + \sigma(r) = \sigma(k+r) = \sigma(n)$.

The skip map. Define $\delta : \mathbb{N} \to \mathbb{N}$ by $\delta(i) = i$ when $i < k$ and $\delta(i) = \sigma(i)$ when $k \le i$; the two clauses are exhaustive and mutually exclusive by trichotomy, so $\delta$ is a function. It is injective: two arguments below $k$ with equal images are equal; two arguments at least $k$ have equal images only if their successors agree, hence only if they agree; and if $i < k \le j$ then $\delta(i) = i < k \le j < \sigma(j) = \delta(j)$.

Splitting law, successor step: $m + \sigma(n) = \sigma(m+n)$, so $\prod_{i<m+\sigma(n)} g_i = \prod_{i<\sigma(m+n)} g_i = \bigl(\prod_{i<m+n} g_i\bigr) \cdot g_{m+n}$; applying the hypothesis and then associativity, this equals $\bigl(\bigl(\prod_{i<m} g_i\bigr) \cdot \prod_{j<n} u_j\bigr) \cdot u_n = \bigl(\prod_{i<m} g_i\bigr) \cdot \bigl(\bigl(\prod_{j<n} u_j\bigr) \cdot u_n\bigr) = \bigl(\prod_{i<m} g_i\bigr) \cdot \prod_{j<\sigma(n)} u_j$, which is the claim at $\sigma(n)$.

$\delta$ maps $n$ into $\sigma(n) \setminus \{k\}$, and onto it. If $i < k$ then $\delta(i) = i \ne k$ and $i < k \le n < \sigma(n)$. If $k \le i < n$ then $\delta(i) = \sigma(i)$ with $k \le i < \sigma(i)$, so $\delta(i) \ne k$, and $i < n$ gives $\sigma(i) < \sigma(n)$ by compatibility of the order with adding $1$. Conversely let $y < \sigma(n)$ with $y \ne k$. If $y < k$ then $y < k \le n$, so $y < n$ and $y = \delta(y)$. If $k < y$ then $y \ne 0$, so $y = \sigma(x)$ for some $x$; from $k < \sigma(x)$ we get $k \le x$, and from $\sigma(x) < \sigma(n)$ we get $x < n$, so $y = \sigma(x) = \delta(x)$ with $x < n$.

By induction the splitting law holds for all $m, n \in \mathbb{N}$; this is claim 1.

The reduced permutation. Set $\pi' := \pi \circ \delta$ restricted to $n$. By step 2.2 it maps $n$ into $\pi[\sigma(n) \setminus \{k\}]$, and since $\pi$ is a bijection of $\sigma(n)$ with $\pi(k) = n$, that image set is $\sigma(n) \setminus \{n\} = n$; the same step gives surjectivity onto it, and $\pi'$ is injective as a composite of injections. So $\pi' \in \operatorname{Sym}(n)$.

Regrouping law, successor step: $\prod_{j<\sigma(r)} B_j = \bigl(\prod_{j<r} B_j\bigr) \cdot B_r = \bigl(\prod_{i<s_r} g_i\bigr) \cdot \prod_{l<c_r} g_{s_r+l}$ by the hypothesis, and the splitting law with $m = s_r$ and $n = c_r$ turns the right-hand side into $\prod_{i<s_r + c_r} g_i = \prod_{i<s_{\sigma(r)}} g_i$. By induction claim 2 holds for every $r$.

Splitting the permuted product. By step 1.9 and the splitting law, $\prod_{i<\sigma(n)} h_i = \prod_{i<k+\sigma(r)} h_i = \bigl(\prod_{i<k} h_i\bigr) \cdot \bigl(\prod_{j<\sigma(r)} h_{k+j}\bigr)$; and since $\sigma(r) = 1 + r$, a second application of the splitting law to the family $j \mapsto h_{k+j}$ gives $\prod_{j<\sigma(r)} h_{k+j} = \bigl(\prod_{j<1} h_{k+j}\bigr) \cdot \bigl(\prod_{l<r} h_{k+1+l}\bigr) = h_k \cdot \prod_{l<r} h_{k+\sigma(l)}$.

Recognising the shorter permuted product. Let $w_i := h_{\delta(i)}$. For $i<k$ one has $w_i = h_i$, and for $l<r$ one has $w_{k+l} = h_{\sigma(k+l)} = h_{k+\sigma(l)}$; so the splitting law at $m = k$, $n = r$ gives $\prod_{i<n} w_i = \bigl(\prod_{i<k} h_i\bigr) \cdot \prod_{l<r} h_{k+\sigma(l)}$. Moreover $w_i = h_{\delta(i)} = g_{\pi(\delta(i))} = g_{\pi'(i)}$ for every $i<n$, by step 2.2 and step 3.2.

Moving the removed factor to the end. $h_k = g_{\pi(k)} = g_n$, and $M$ is commutative, so $\bigl(\prod_{i<k} h_i\bigr) \cdot \bigl(h_k \cdot \prod_{l<r} h_{k+\sigma(l)}\bigr) = \bigl(\bigl(\prod_{i<k} h_i\bigr) \cdot \prod_{l<r} h_{k+\sigma(l)}\bigr) \cdot g_n$, using commutativity to exchange $h_k$ with the block to its right and associativity to regroup.

Applying the hypothesis. The family $w$ satisfies $w_i = g_{\pi'(i)}$ for $i<n$ with $\pi' \in \operatorname{Sym}(n)$, so the inductive hypothesis gives $\prod_{i<n} w_i = \prod_{i<n} g_i$; combining with steps 4.2, 5.1 and 4.3, $\prod_{i<\sigma(n)} h_i = \bigl(\prod_{i<n} g_i\bigr) \cdot g_n = \prod_{i<\sigma(n)} g_i$, which is the claim at $\sigma(n)$.

By induction claim 3 holds for every $n$; with claims 1 and 2 already established, the theorem is proved.