I'm working on a proof of $\prod_{\alpha\in\Lambda}\overline{A_\alpha}=\overline{\prod_{\alpha\in\Lambda}A_\alpha}$ in the product topology. This has been asked before, i.e. Closure in a product of topological spaces, The closure of a product is the product of closures? but they aren't explicit on the parts which are giving me trouble.
If $(C_\alpha)_{\alpha\in\Lambda}$ is a collection of closed sets, the product $\prod_{\alpha\in\Lambda}C_\alpha$ can be written as $\bigcap_{\alpha\in\Lambda}\pi_\alpha^{-1}(C_\alpha)$, and continuity of $\pi_\alpha$ implies $\pi_\alpha^{-1}(C_\alpha)$ is closed, so $\prod_{\alpha\in\Lambda}C_\alpha$ is also closed. Setting $C_\alpha=\overline{A_\alpha}$ this proves $\prod_{\alpha\in\Lambda}\overline{A_\alpha}\supseteq\overline{\prod_{\alpha\in\Lambda}A_\alpha}$.
For the reverse inclusion, suppose $x=(x_\alpha)_{\alpha\in\Lambda}\in\prod_{\alpha\in\Lambda}\overline{A_\alpha}$, and let $U=\prod_{\alpha\in\Lambda}U_\alpha$ be a basic open set containing $x$, with $I\subseteq \Lambda$ finite such that $U_\alpha=X_\alpha$ for $\alpha\notin I$. Since $x_\alpha\in \overline{A_\alpha}\cap U_\alpha$, there is a $y_\alpha\in A_\alpha\cap U_\alpha$, so an application of the axiom of choice would give a $y=(y_\alpha)_{\alpha\in\Lambda}\in$ $\prod_{\alpha\in\Lambda}A_\alpha\cap U$ as desired.
Is AC necessary here? So far I haven't even been able to show that $\prod_{\alpha\in\Lambda}\overline{A_\alpha}\ne\emptyset$ implies $\prod_{\alpha\in\Lambda}A_\alpha\ne\emptyset$, and surely the theorem can't be proven without establishing this.