The sum rule: a finite disjoint union is finite with $\mid A\cup B\mid =\mid A\mid +\mid B\mid$ and $\mid {\bigcup }_{i\in I}{A}_i\mid ={\sum }_{i\in I}\mid A_i\mid$, and a sum over a finite index set splits along a partition

The splice map. Let $A$, $B$ be finite and disjoint, put $p:=\mid A\mid$, $q:=\mid B\mid$, 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=\mathrm{\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=\mathrm{\varnothing }$ has empty union, so $\mid {\bigcup }_{k<0}{B}_k\mid =\mid \mathrm{\varnothing }\mid =0={\sum }_{k<0}\mid B_k\mid$; and a partition of $S$ indexed by $0$ forces $S=\mathrm{\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}\mid B_k\mid$; and for a partition of a finite set $S$ into pairwise disjoint $S_0,\dots ,S_{m-1}$ one has ${\mathrm{★}}_{i\in S}{a}_i={\mathrm{★}}_{k<m}\left({\mathrm{★}}_{i\in S_k}{a}_i\right)$.

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 $\mid A\cup B\mid =\mid p+q\mid =p+q=\mid A\mid +\mid B\mid$.

Clause 3 for two blocks. Let $S$, $T$ be finite and disjoint and $a$ defined on $S\cup T$. With $p=\mid S\mid$, $q=\mid T\mid$ and the bijections $f,g,h$ of step 1.1 for the pair $S$, $T$, step 2.1 gives $\mid S\cup T\mid =p+q$, so $h$ may be used as the enumeration in [L3]. Then ${\mathrm{★}}_{i\in S\cup T}{a}_i={\mathrm{★}}_{k<p+q}{a}_{h(k)}=\left({\mathrm{★}}_{k<p}{a}_{h(k)}\right)\ast \left({\mathrm{★}}_{j<q}{a}_{h(p+j)}\right)=\left({\mathrm{★}}_{k<p}{a}_{f(k)}\right)\ast \left({\mathrm{★}}_{j<q}{a}_{g(j)}\right)=\left({\mathrm{★}}_{i\in S}{a}_i\right)\ast \left({\mathrm{★}}_{i\in T}{a}_i\right)$, 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=\left({\bigcup }_{k<m}{B}_k\right)\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}\mid B_k\mid$, so clause 1 makes the union finite with cardinality ${\sum }_{k<m}\mid B_k\mid +\mid B_m\mid ={\sum }_{k<\sigma (m)}\mid B_k\mid$ 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 $\phi :m\to I$ with $m=\mid I\mid$; then ${\bigcup }_{i\in I}{A}_i={\bigcup }_{k<m}{A}_{\phi (k)}$ and ${\sum }_{i\in I}\mid A_i\mid ={\sum }_{k<m}\mid A_{\phi (k)}\mid$ 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^{\mathrm{\prime }}:={\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^{\mathrm{\prime }}$ into $S_0,\dots ,S_{m-1}$, and step 3.1 applies to the disjoint pair $S^{\mathrm{\prime }}$, $S_m$, giving ${\mathrm{★}}_{i\in S}{a}_i=\left({\mathrm{★}}_{i\in S^{\mathrm{\prime }}}{a}_i\right)\ast \left({\mathrm{★}}_{i\in S_m}{a}_i\right)=\left({\mathrm{★}}_{k<m}{\mathrm{★}}_{i\in S_k}{a}_i\right)\ast \left({\mathrm{★}}_{i\in S_m}{a}_i\right)={\mathrm{★}}_{k<\sigma (m)}\left({\mathrm{★}}_{i\in S_k}{a}_i\right)$ 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.