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 \left({\prod }_{k<p}{X}_k\right)\times X_p$ by $r(x):=(x\upharpoonright 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\mathrm{\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=\mathrm{\varnothing }$ being covered by $\mathcal{V}=\mathrm{\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\upharpoonright 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=\mathrm{\varnothing }$ then $X\times Z=\mathrm{\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 \cdots \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 $\left({\prod }_{k<p}{X}_k\right)\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 \cdots \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 $\left({\prod }_{k<m}{X}_k\right)\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$.