The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition

The splice map. Let $A$, $B$ be finite and disjoint, put $p := \lvert A\rvert$, $q := \lvert B\rvert$, and fix bijections $f : p \to A$ and $g : q \to B$. Define $h : p + q \to A \cup B$ by $h(k) = f(k)$ when $k < p$, and, when $p \le k$, by $h(k) = g(j)$ for the unique $j$ with $p + j = k$; that $j$ satisfies $j < q$ because $p + j = k < p + q$. The map $h$ is well defined by [L6], it is surjective because every element of $A \cup B$ is some $f(k)$ or some $g(j)$, and it is injective: two indices below $p$ are separated by the injectivity of $f$, two indices at least $p$ by the injectivity of $g$ together with the uniqueness of $j$, and an index below $p$ from one at least $p$ because $f(k) \in A$, $g(j) \in B$ and $A \cap B = \varnothing$. The last of these three cases is the only use of disjointness in the whole proof.

Base cases of the two inductions below, at $m = 0$. A family indexed by $0 = \varnothing$ has empty union, so $\big\lvert\bigcup_{k<0} B_k\big\rvert = \lvert\varnothing\rvert = 0 = \sum_{k<0}\lvert B_k\rvert$; and a partition of $S$ indexed by $0$ forces $S = \varnothing$, so both sides of clause 3 are $e$.

Inductive hypothesis for both inductions, at $m$: for pairwise disjoint finite $B_0, \dots, B_{m-1}$ the union $\bigcup_{k<m} B_k$ is finite with cardinality $\sum_{k<m}\lvert B_k\rvert$; and for a partition of a finite set $S$ into pairwise disjoint $S_0, \dots, S_{m-1}$ one has $\bigstar_{i \in S} a_i = \bigstar_{k<m}\big(\bigstar_{i \in S_k} a_i\big)$.

Clause 1. By step 1.1 the map $h$ is a bijection $p + q \to A \cup B$, so $A \cup B \approx p+q$; hence $A \cup B$ is finite and $\lvert A \cup B\rvert = \lvert p+q\rvert = p + q = \lvert A\rvert + \lvert B\rvert$.

Clause 3 for two blocks. Let $S$, $T$ be finite and disjoint and $a$ defined on $S \cup T$. With $p = \lvert S\rvert$, $q = \lvert T\rvert$ and the bijections $f, g, h$ of step 1.1 for the pair $S$, $T$, step 2.1 gives $\lvert S \cup T\rvert = p+q$, so $h$ may be used as the enumeration in [L3]. Then $\bigstar_{i \in S \cup T} a_i = \bigstar_{k<p+q} a_{h(k)} = \big(\bigstar_{k<p} a_{h(k)}\big) \ast \big(\bigstar_{j<q} a_{h(p+j)}\big) = \big(\bigstar_{k<p} a_{f(k)}\big) \ast \big(\bigstar_{j<q} a_{g(j)}\big) = \big(\bigstar_{i \in S} a_i\big) \ast \big(\bigstar_{i \in T} a_i\big)$, using [L5] at the second equality.

Inductive step for clause 2, in the case of an index set $\sigma(m)$. Let $B_0, \dots, B_{m}$ be pairwise disjoint and finite. Then $\bigcup_{k<\sigma(m)} B_k = \big(\bigcup_{k<m} B_k\big) \cup B_m$, and these two sets are disjoint because each $B_k$ with $k < m$ is disjoint from $B_m$. By the hypothesis of step 1.3 the first is finite with cardinality $\sum_{k<m}\lvert B_k\rvert$, so clause 1 makes the union finite with cardinality $\sum_{k<m}\lvert B_k\rvert + \lvert B_m\rvert = \sum_{k<\sigma(m)}\lvert B_k\rvert$ by [L4].

Clause 2. By step 1.2, step 3.2 and induction, the statement holds for every family indexed by a natural number $m$. For a general finite index set $I$ take a bijection $\varphi : m \to I$ with $m = \lvert I\rvert$; then $\bigcup_{i \in I} A_i = \bigcup_{k<m} A_{\varphi(k)}$ and $\sum_{i \in I}\lvert A_i\rvert = \sum_{k<m}\lvert A_{\varphi(k)}\rvert$ by the definition of the sum over a finite index set, so the two statements coincide.

Inductive step for clause 3, index set $\sigma(m)$. Let $S$ be finite and partitioned into pairwise disjoint $S_0, \dots, S_m$, and put $S' := \bigcup_{k<m} S_k$, which is finite by [L8] and disjoint from $S_m$. The hypothesis of step 1.3 applies to the partition of $S'$ into $S_0, \dots, S_{m-1}$, and step 3.1 applies to the disjoint pair $S'$, $S_m$, giving $\bigstar_{i \in S} a_i = \big(\bigstar_{i \in S'} a_i\big) \ast \big(\bigstar_{i \in S_m} a_i\big) = \big(\bigstar_{k<m}\bigstar_{i \in S_k} a_i\big) \ast \big(\bigstar_{i \in S_m} a_i\big) = \bigstar_{k<\sigma(m)}\big(\bigstar_{i \in S_k} a_i\big)$ by [L4].

Clause 3. By step 1.2, step 5.1 and induction it holds for every index set that is a natural number, and the general finite $J$ follows by reindexing along a bijection $m \to J$ exactly as in step 4.1. The two-block form is step 3.1.

Clause 1 is step 2.1, clause 2 is step 4.1 and clause 3 is step 6.1; since $\ast$ was an arbitrary one of the four operations, both the sum and the product forms of clause 3 are proved.