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!