Tychonoff's theorem for products of finite discrete topologies?

Question

I need the following specific version of Tychonoff's theorem:

Suppose $\{X_\alpha\}_\alpha$ is a collection of finite sets endowed with discrete topologies, then $\prod_\alpha X_\alpha$ is compact.

I wonder whether there's any direct proof for this specific version, since it's pervasive in mathematics (other than general topology), say the theory of pro-finite groups where infinite Galois theory is based. Many existence theorem is deduced from compactness.

I wonder whether there are more direct proofs (but Zorn's lemma is allowed) for this special case. I don't like base many existence theorems (especially some existence of a specific morphism between extension fields) on the black box of Tychonoff's theorem.

For example, suppose $A$ is an integrally closed domain with quotient field $F$, and $K/F$ is a normal extension. Let $B$ be the integral closure of $A$ in $K$. Given a prime ideal $P\subsetneq A$, we want to show that $\operatorname{Gal}(K/F)$ acts transitively on prime ideals lying over $P$. We can first prove it for finite extension $K/F$, and deduce the general case from this special case by compactness of $\operatorname{Gal}(K/F)$, see Serre's Local Algebra, say. However, I want to see how this Galois element is constructed without appealing to Tychonoff's theorem.

Any help is welcome. Thanks!

Answer 1

It seems possibly interesting to note that the compactness of an arbitrary product of finite sets gives a "direct" proof of the compactness of a product of arbitrary compact Hausdorff spaces (hence, regardless of what we mean by "direct" in the OP, the result for finite sets can't be much easier than the Tychonoff theorem itself.)

Since the Cantor set $K$ is a countable product of $\{0,1\}$, the compactness of $\prod X_\alpha$ for $X_\alpha=\{0,1\}$ implies the compactness of the product for $X_\alpha=K$. Now there is a continuous map from $K$ onto $[0,1]$, so we get the result for $X_\alpha=[0,1]$. And any compact Hausdorff space can be embedded in a (high-dimensional) cube, hence if $X_\alpha$ is compact Hausdorff then $\prod X_\alpha$ is a closed subset of a compact Hausdorff space.