The multinomial coefficient equals $n!/\prod_{i<m} k_i!$, and $(x_0+\dots+x_{m-1})^{n} = \sum \iota\!\binom{n}{k}\prod_{i<m} x_i^{k_i}$ in $\mathbb{R}$

Notation for both inductions. For $m = \sigma(M)$ and $k \in \mathcal{W}(n,\sigma(M))$, splitting the sum at index $1$ ([L5]) gives $n = \sum_{i<\sigma(M)}k_i = k_0 + \sum_{j<M} k'_j$, so $k' \in \mathcal{W}(n - k_0, M)$ and $k_0 \le n$; the same splitting for products gives $\prod_{i<\sigma(M)}k_i! = k_0!\cdot\prod_{j<M}k'_j!$.

Base case of clause 1, at $m = 0$. Then $\mathcal{W}(n,0)$ is nonempty only for $n = 0$, and there $\binom{0}{\ } = 1$, the empty product of factorials is $1$ and $0! = 1$, so the identity reads $1 \cdot 1 = 1$.

Inductive hypothesis for clause 1: fix $M$ and assume $\binom{N}{k'}\prod_{j<M}k'_j! = N!$ for every $N$ and every $k' \in \mathcal{W}(N,M)$.

Base case of clause 2, at $m = 0$. The left-hand side is $\big(\sum_{i<0}x_i\big)^{n} = 0^{\,n}$. If $n = 0$ this is $1$, and the right-hand side is the single term $\iota\binom{0}{\ }\prod_{i<0}x_i^{k_i} = 1\cdot 1 = 1$. If $n \ge 1$ then $0^{\,n} = 0$ and $\mathcal{W}(n,0) = \varnothing$, so the right-hand side is an empty sum, equal to $0$.

Inductive step for clause 1. Let $m = \sigma(M)$, $k \in \mathcal{W}(n,\sigma(M))$, and let $A$ be finite with $\lvert A\rvert = n$. The map $c \mapsto \big(c^{-1}[\{0\}],\, c''\big)$, where $c''(a)$ is the unique $i$ with $c(a) = \sigma(i)$ for $a \notin c^{-1}[\{0\}]$, sends $\mathcal{B}(A,k)$ to the set of pairs $(S, c'')$ with $S \in [A]^{k_0}$ and $c'' \in \mathcal{B}(A\setminus S, k')$; it is well defined because $c(a) \ne 0$ off the first fibre, every nonzero natural is a unique successor, and $\lvert c''^{-1}[\{j\}]\rvert = \lvert c^{-1}[\{\sigma(j)\}]\rvert = k'_j$. Its two-sided inverse sends $(S,c'')$ to the colouring equal to $0$ on $S$ and to $\sigma(c''(a))$ off $S$. The pairs form the union of the pairwise disjoint sets $\{S\}\times\mathcal{B}(A\setminus S,k')$ indexed by $S \in [A]^{k_0}$, and $\lvert A\setminus S\rvert = n-k_0$ by [L3], so each has $\binom{n-k_0}{k'}$ elements. Hence $\binom{n}{k} = \binom{n}{k_0}\binom{n-k_0}{k'}$ by [L3] and [L8]. Multiplying by $\prod_{i<\sigma(M)}k_i! = k_0!\prod_{j<M}k'_j!$ and using the hypothesis of step 1.3 at $N = n-k_0$ gives $\binom{n}{k}\prod_{i<\sigma(M)}k_i! = \binom{n}{k_0}\,k_0!\cdot\Big(\binom{n-k_0}{k'}\prod_{j<M}k'_j!\Big) = \binom{n}{k_0}\,k_0!\,(n-k_0)! = n!$ by [L4], since $k_0 \le n$.

Clause 1 holds for every $m$, by step 1.2, step 2.1 and induction. The real form follows: applying $\iota$ gives $\iota\binom{n}{k}\prod_{i<m}\iota(k_i!) = \iota(n!)$, and each $\iota(k_i!)$ is nonzero by [L6] and [L7], so the product is invertible in $\mathbb{R}$.

Inductive step for clause 2. Assume clause 2 at $M$, for every $n$ and every list of length $M$. Let $x : \sigma(M) \to \mathbb{R}$, put $y := \sum_{i<M}x_i$ and $z := x_M$, so $\sum_{i<\sigma(M)}x_i = y + z$ by [L5]. The map $\Phi(j,\kappa) := \widehat{\kappa}$, where $\widehat{\kappa}$ restricts to $\kappa$ on $M$ and $\widehat{\kappa}_M := n-j$, is a bijection from the disjoint union of the sets $\{j\}\times\mathcal{W}(j,M)$, $j < \sigma(n)$, onto $\mathcal{W}(n,\sigma(M))$: it lands there because $\sum_{i<\sigma(M)}\widehat{\kappa}_i = j + (n-j) = n$, and its inverse sends $\widehat{\kappa}$ to the pair $\big(\sum_{i<M}\widehat{\kappa}_i,\ \widehat{\kappa}\restriction M\big)$, the two constructions being mutually inverse by [L8]. Moreover $\iota\binom{n}{j}\,\iota\binom{j}{\kappa} = \iota\binom{n}{\widehat{\kappa}}$: by step 3.1 and [L4], both $\binom{n}{\widehat{\kappa}}$ and $\binom{n}{j}\binom{j}{\kappa}$ become $n!$ after multiplication by the nonzero natural $\big(\prod_{i<M}\kappa_i!\big)(n-j)!$, so they are equal by cancellation. And $\prod_{i<M}x_i^{\kappa_i}\cdot z^{\,n-j} = \prod_{i<\sigma(M)}x_i^{\widehat{\kappa}_i}$ by the product recursion clause. Now [L4] gives $(y+z)^{n} = \sum_{j<\sigma(n)}\iota\binom{n}{j}y^{\,j}z^{\,n-j}$; substituting the inductive hypothesis for $y^{\,j}$, distributing the scalar $\iota\binom{n}{j}z^{\,n-j}$ over the inner sum by the scaling clause of [L5], and then applying [L3] to the partition of $\mathcal{W}(n,\sigma(M))$ into the images of the sets $\mathcal{W}(j,M)$ under $\Phi$ yields $\big(\sum_{i<\sigma(M)}x_i\big)^{n} = \sum_{\widehat{\kappa}\in\mathcal{W}(n,\sigma(M))}\iota\binom{n}{\widehat{\kappa}}\prod_{i<\sigma(M)}x_i^{\widehat{\kappa}_i}$.

By step 1.4, step 4.1 and induction, clause 2 holds for every $m \in \mathbb{N}$, every $n$ and every list $x$.

Clause 1 is step 3.1 and clause 2 is step 5.1.