2 Mention Tychonoff's original theorem

Inspired by some of the comments, I would nominate the definition of infinite product topology in terms of its open sets, found in, e.g., Munkres' otherwise excellent Topology. "The product topology on $X = \prod_{\alpha \in J} X_\alpha$ is the topology generated by the sets of the form $\pi_\alpha^{-1}(U_\alpha)$, where $U_\alpha$ is an open subset of $X_\alpha$." One then proves that one can also use the basis of sets of the form $U = \prod_{\alpha \in J} U_\alpha$ where $U_\alpha$ is open in $X_\alpha$, and $U_\alpha = X_\alpha$ for all but finitely many $\alpha \in J$. This just makes it look like an annoying and unnatural modification of the box topology.

Better in my opinion is to view $X = \prod X_\alpha$ explicitly as a function space (not as some sort of tuples, though they are really functions underneath), and to use the terminology of nets. Then it becomes clear that the product topology is just the topology of pointwise convergence, i.e. a net $f_i \to f$ iff the nets $f_i(\alpha) \to f(\alpha)$ for all $\alpha \in J$.

Under this definition, Tychonoff's theorem, which previously seemed pretty obscure, has an obvious application when combined with Heine-Borel: given any set $J$ and a pointwise bounded net of functions $f_i : J \to \mathbb{R}$, there is a subnet that converges pointwise. This is maybe the most useful application, especially in functional analysis. (Indeed, I understand this was actually Tychonoff's original theorem, that an arbitrary product of closed intervals is compact.) For instance, it makes Alaoglu's theorem clear, once you see that the weak-* topology is just a toplogy of pointwise convergence.

It's nice then to compare this with the Arzela-Ascoli theorem, which says that if $J$ is a compact Hausdorff space and the functions $f_i$ are not only pointwise bounded but also continuous and equicontinuous, then a subnet (in fact a subsequence) converges not only pointwise but in fact uniformly.

Inspired by some of the comments, I would nominate the definition of infinite product topology in terms of its open sets, found in, e.g., Munkres' otherwise excellent Topology. "The product topology on $X = \prod_{\alpha \in J} X_\alpha$ is the topology generated by the sets of the form $\pi_\alpha^{-1}(U_\alpha)$, where $U_\alpha$ is an open subset of $X_\alpha$." One then proves that one can also use the basis of sets of the form $U = \prod_{\alpha \in J} U_\alpha$ where $U_\alpha$ is open in $X_\alpha$, and $U_\alpha = X_\alpha$ for all but finitely many $\alpha \in J$. This just makes it look like an annoying and unnatural modification of the box topology.
Better in my opinion is to view $X = \prod X_\alpha$ explicitly as a function space (not as some sort of tuples, though they are really functions underneath), and to use the terminology of nets. Then it becomes clear that the product topology is just the topology of pointwise convergence, i.e. a net $f_i \to f$ iff the nets $f_i(\alpha) \to f(\alpha)$ for all $\alpha \in J$.
Under this definition, Tychonoff's theorem, which previously seemed pretty obscure, has an obvious application when combined with Heine-Borel: given any set $J$ and a pointwise bounded net of functions $f_i : J \to \mathbb{R}$, there is a subnet that converges pointwise. This is maybe the most useful application, especially in functional analysis. For instance, it makes Alaoglu's theorem clear, once you see that the weak-* topology is just a toplogy of pointwise convergence.
It's nice then to compare this with the Arzela-Ascoli theorem, which says that if $J$ is a compact Hausdorff space and the functions $f_i$ are not only pointwise bounded but also continuous and equicontinuous, then a subnet (in fact a subsequence) converges not only pointwise but in fact uniformly.