Solution (source code)

= Solution

First assume \b[both factors are nonempty]. If the product is <compact>, its <continuous> coordinate projections are onto, so each factor is <compact> by the <continuous image of a compact space> theorem.

For the converse, let $X,Y$ be <compact> and let $(W_\lambda)$ be an <open> cover of their product. Fix $x\in X$. For every $y\in Y$, choose a <basis> rectangle $U_{x,y}\times V_{x,y}$ containing $(x,y)$ and lying in a cover member $W_{\lambda(x,y)}$. <Compactness> of $Y$ gives finitely many $V_{x,y_j}$ covering $Y$. Then
$$
U_x=\bigcap_jU_{x,y_j}
$$
is an <open neighbourhood> of $x$, and $U_x\times Y$ is covered by the corresponding finitely many $W_{\lambda(x,y_j)}$.

The sets $U_x$ cover $X$. <Compactness> gives finitely many of them covering $X$, and the finitely many cover members associated to these choices now cover $X\times Y$. Hence the product is <compact>. This is the finite-product <Tychonoff theorem> proof, with the <finite intersection> creating a uniform neighbourhood along each fibre.

As printed, the assertion omits the nonempty hypothesis. If $X=\varnothing$ and $Y=\mathbb R$, the product is <compact> while $Y$ is not. The fully correct version without any nonemptiness assumption is
$$
\boxed{X\times Y\text{ compact}\iff X=\varnothing\text{ or }Y=\varnothing\text{ or both factors are compact}.}
$$