A finite sum is unchanged by a permutation of its index range: $\sum_{k<n} a_{\pi(k)} = \sum_{k<n} a_k$ for every bijection $\pi : n \to n$

For $n \in \mathbb{N}$ and $j \le n$ define $d^{n}_{j} : n \to \sigma(n)$ by $d^{n}_{j}(k) = k$ for $k < j$ and $d^{n}_{j}(k) = \sigma(k)$ for $j \le k < n$; this is the increasing enumeration of $\sigma(n) \setminus \{j\}$. It is a bijection of $n$ onto $\sigma(n) \setminus \{j\}$: its values lie in $\sigma(n)$ and avoid $j$, since $k < j$ in the first clause and $\sigma(k) > k \ge j$ in the second; it is injective, being strictly increasing on each clause and satisfying $k < j \le \sigma(k')$ across them; and it is surjective, since $t \in \sigma(n)$ with $t < j$ has $t < n$ and $d^{n}_{j}(t) = t$, while $t > j$ is nonzero, so $t = \sigma(s)$ with $j \le s$ by [L5] and $s < n$ because $\sigma(s) \le n$, giving $d^{n}_{j}(s) = t$.

Claim $(A)$ at $n = 0$: for a list $c$ of length $\sigma(0) = 1$ and the only admissible index $j = 0$, both sides of $(A)$ read $c_0$, since $\bigstar_{k<1} c_k = e \ast c_0 = c_0$ and $\big(\bigstar_{k<0} c_{d^{0}_{0}(k)}\big) \ast c_0 = e \ast c_0 = c_0$.

Inductive hypothesis for $(A)$: fix $n$ and assume that for every list $c$ of length $\sigma(n)$ and every $j \le n$ one has $\bigstar_{k<\sigma(n)} c_k = \big(\bigstar_{k<n} c_{d^{n}_{j}(k)}\big) \ast c_j$.

The main claim at $n = 0$: the only bijection $0 \to 0$ is the empty map and both sides are the empty iterate $e$.

Inductive step for $(A)$. Let $c$ be a list of length $\sigma(\sigma(n))$ and let $j \le \sigma(n)$. If $j = \sigma(n)$ then $d^{\sigma(n)}_{j}$ is the identity of $\sigma(n)$, so the right-hand side is $\big(\bigstar_{k<\sigma(n)} c_k\big) \ast c_{\sigma(n)}$, which is the left-hand side by [L2]. If instead $j \le n$, apply the hypothesis of step 1.3 to the restriction of $c$ to $\sigma(n)$ to get $\bigstar_{k<\sigma(n)} c_k = \big(\bigstar_{k<n} c_{d^{n}_{j}(k)}\big) \ast c_j$; hence $\bigstar_{k<\sigma(\sigma(n))} c_k = \big(\big(\bigstar_{k<n} c_{d^{n}_{j}(k)}\big) \ast c_j\big) \ast c_{\sigma(n)} = \big(\big(\bigstar_{k<n} c_{d^{n}_{j}(k)}\big) \ast c_{\sigma(n)}\big) \ast c_j$ by [L3]. Finally $d^{\sigma(n)}_{j}$ agrees with $d^{n}_{j}$ on $n$ and sends $n$ to $\sigma(n)$, because $j \le n$, so the inner bracket is $\bigstar_{k<\sigma(n)} c_{d^{\sigma(n)}_{j}(k)}$ by [L2], which is the right-hand side at $\sigma(n)$.

Claim $(A)$ therefore holds for every $n$: for every list $c$ of length $\sigma(n)$ and every $j \le n$, $\bigstar_{k<\sigma(n)} c_k = \big(\bigstar_{k<n} c_{d^{n}_{j}(k)}\big) \ast c_j$. Informally, any single entry may be moved to the end without changing the value.

Inductive step for the main claim. Assume it at $n$, for every list of length $n$ and every bijection of $n$. Let $\pi : \sigma(n) \to \sigma(n)$ be a bijection, let $a$ be a list of length $\sigma(n)$, and put $j := \pi^{-1}(n) \le n$. Applying $(A)$ to the list $c_k := a_{\pi(k)}$ at the index $j$ gives $\bigstar_{k<\sigma(n)} a_{\pi(k)} = \big(\bigstar_{k<n} a_{\rho(k)}\big) \ast a_{\pi(j)}$ with $\rho := \pi \circ d^{n}_{j}$ and $a_{\pi(j)} = a_n$. Now $\rho$ is a bijection of $n$ onto $n$: $d^{n}_{j}$ is a bijection of $n$ onto $\sigma(n)\setminus\{j\}$ by step 1.1, and $\pi$ restricts to a bijection of $\sigma(n)\setminus\{j\}$ onto $\sigma(n)\setminus\{n\} = n$. So the inductive hypothesis applies to $\rho$ and gives $\bigstar_{k<n} a_{\rho(k)} = \bigstar_{k<n} a_k$, whence $\bigstar_{k<\sigma(n)} a_{\pi(k)} = \big(\bigstar_{k<n} a_k\big) \ast a_n = \bigstar_{k<\sigma(n)} a_k$.

By induction the main claim holds for every $n \in \mathbb{N}$, every list of length $n$ and every bijection $\pi : n \to n$.

Since $\ast$ was any one of the four operations of the Given, and [L3] holds for each of them, step 5.1 is exactly clauses 1 and 2.