A product of finitely many compact spaces is compact in the product topology

At $n = 0$ the index set is empty, so $\prod_{k<0} X_k$ is a one-point space by [A1] and is compact by [L8]; this is the case $n = 0$ of the statement.

Let $m \in \mathbb{N}$ and assume, as the induction hypothesis, that $\prod_{k<m} Y_k$ is compact for every family $(Y_k)_{k<m}$ of compact spaces.

For the binary case let $X$ and $Z$ be compact, let $\mathcal{U}$ be an open cover of $X \times Z$, and for $z \in Z$ let $j_z : X \to X \times Z$ be $j_z(x) := (x,z)$; its components are the identity of $X$ and the constant map with value $z$, so it is continuous by [L1] and [L3], and $X \times \{z\} = j_z[X]$ is therefore a compact subset of $X \times Z$ by [L4].

Put $\mathcal{W} := \{\, W \subseteq Z : W \text{ is open and } X \times W \subseteq \bigcup \mathcal{V} \text{ for some finite } \mathcal{V} \subseteq \mathcal{U} \,\}$, a family cut out by a property of $W$ and not by any selection.

For the splitting, let $p \in \mathbb{N}$, let $(X_k)_{k < \sigma(p)}$ be a family of spaces, and define $r : \prod_{k<\sigma(p)} X_k \to \big(\prod_{k<p} X_k\big) \times X_p$ by $r(x) := (x \restriction p,\ x(p))$ and $s$ in the opposite direction by $s(y,a) := y \cup \{(p,a)\}$; by [A1] these are mutually inverse bijections, since $\sigma(p) = p \cup \{p\}$ and $p \notin p$.

$Z \subseteq \bigcup \mathcal{W}$: given $z \in Z$, the set $X \times \{z\}$ is compact by step 1.3 and lies in $\bigcup \mathcal{U}$, so [L6] supplies a finite $\mathcal{V} \subseteq \mathcal{U}$ with $X \times \{z\} \subseteq N := \bigcup \mathcal{V}$, an open set, the case $X = \varnothing$ being covered by $\mathcal{V} = \varnothing$; since $X$ is compact, [L5] gives an open $W \ni z$ with $X \times W \subseteq N$, and that $W$ lies in $\mathcal{W}$.

$r$ is continuous: by [L1] it suffices that its two components are, and they are $x \mapsto x \restriction p$ and $\pi_p$; the second is a projection, and the first is continuous by [L1] applied again, its own components being $\pi_k$ for $k < p$.

$s$ is continuous: by [L1] it suffices that $\pi_k \circ s$ is continuous for every $k < \sigma(p)$; for $k < p$ that map is the $k$-th projection of $\prod_{k<p} X_k$ composed with the first projection of the binary product, a composite of continuous maps, and for $k = p$ it is the second projection of the binary product.

If $Z = \varnothing$ then $X \times Z = \varnothing$ is compact by [L8]; otherwise $\mathcal{W}$ is an open cover of the compact $Z$ by step 2.1, so [L8] gives $q \in \mathbb{N}$ and $W_0, \dots, W_q \in \mathcal{W}$ with $Z = W_0 \cup \dots \cup W_q$.

So $r$ is a continuous bijection with continuous inverse $s$, hence a homeomorphism, and $\prod_{k<\sigma(p)} X_k$ is homeomorphic to $\big(\prod_{k<p} X_k\big) \times X_p$.

For each $j \le q$ the set $T_j$ of finite subfamilies $\mathcal{V} \subseteq \mathcal{U}$ with $X \times W_j \subseteq \bigcup \mathcal{V}$ is nonempty because $W_j \in \mathcal{W}$, and $j \mapsto T_j$ is a function with domain the natural number $\sigma(q)$, so [L7] supplies $\mathcal{V}_0, \dots, \mathcal{V}_q$; their union $\mathcal{V}$ is a finite subfamily of $\mathcal{U}$, a union of finitely many listable families being listed by concatenation, and $X \times Z = (X \times W_0) \cup \dots \cup (X \times W_q) \subseteq \bigcup \mathcal{V}$. So every open cover of $X \times Z$ has a finite subcover and $X \times Z$ is compact.

Now let $(X_k)_{k < \sigma(m)}$ be a family of compact spaces. By step 1.2 the product $\prod_{k<m} X_k$ is compact, and $X_m$ is compact, so step 4.1 makes $\big(\prod_{k<m} X_k\big) \times X_m$ compact; by step 3.2 with $p := m$ the product $\prod_{k<\sigma(m)} X_k$ is homeomorphic to it, and a continuous image of a compact space is compact by [L4], so $\prod_{k<\sigma(m)} X_k$ is compact.

The set of $n \in \mathbb{N}$ for which the statement holds contains $0$ by step 1.1 and contains $\sigma(m)$ whenever it contains $m$ by step 5.1, so by [L9] it is all of $\mathbb{N}$; the binary case is $n = 2$ and the empty product is $n = 0$.