Arbitrary products of completely regular spaces are completely regular

Given: A product $P=\prod_{i\in I}X_i$ of completely regular spaces, a closed $C\subseteq P$, and $x\in P\setminus C$.

A basic product-open set has finite support, and the product universal property makes finite-coordinate maps continuous (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

Complete regularity gives $h_i:X_i\to[0,1]$ with $h_i(x_i)=1$ and $h_i[X_i\setminus U_i]=\{0\}$ when $x_i\in U_i$ is open (Completely regular spaces and Tychonoff ($T_{3\frac{1}{2}}$) spaces).

A finite pointwise minimum of continuous $[0,1]$-valued maps is continuous (Finite pointwise minima of continuous maps to $[0,1]$ are continuous).

A family indexed by a natural number whose members are nonempty has a choice function, without any choice axiom (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).