$X^\omega$ is separable if $X$ is separable How should one interpret the following proof:

I don't get the proof that $X^\omega$ (under the product topology) is separable if $X$ is separable. In fact, I'm not sure what topology $X$ is supposed to have. The context is Polish spaces. Maybe someone with more experience in descriptive set theory recognizes what I'm missing here?
 A: It doesn’t matter what the topology on $X$ is, so long as it is separable. A basic open set $B$ in ${^\omega}X$ has the following form: there are a finite $F\subseteq\omega$ and open sets $U_k$ in $X$ for each $k\in F$ such that
$$B=\left\{\bar x\in{^\omega}X:\bar x_k\in U_k\text{ for each }k\in F\right\}\,.$$
The family $\{z_n:n\in\omega\}$ is dense in $X$, so for each $k\in F$ there is an $n(k)\in\omega$ such that $z_{n(k)}\in U_k$.
The set $B_0=\left\{f\in{^\omega}\omega:f(k)=n(k)\text{ for each }k\in F\right\}$ is a basic open set in the Baire space ${^\omega}\omega$, and $D$ is dense in ${^\omega}\omega$, so $f\in B_0\cap D\ne\varnothing$. Let $f\in B_0\cap D$; then $\bar z_f(k)=z_{f(k)}=z_{n(k)}$ for each $k\in F$, so $\bar z_f\in B$.
Thus, each basic open set in ${^\omega}X$ contains a member of the countable set $\{\bar z_f:f\in D\}$, and ${^\omega}X$ is therefore separable.
A: I suspect the source of the confusion is the introduction of Baire space in the course of the argument, which if read quickly suggests that $X$ itself is assumed to be related to Baire space somehow. But this isn't the case: Baire space is really just functioning as a "bookkeeping tool" to give a concrete description of the construction of a countable dense subset of $X^\omega$ from a countable dense subset of $X$.
If you like, we can get rid of any mention of Baire space as follows (although the argument is really identical). Suppose $U\subseteq X^\omega$ is a (nonempty) basic open set. Then $$U=\prod_{i\in\omega} V_i$$ for some sequence of open sets $(V_i)_{i\in\omega}$ such that all but finitely many of the $V_i$s are just $X$ itself.$^1$ Fix a countable dense subset $\{x_j:j\in\omega\}$ of $X$. Then to each basic open $U$ we can assign a "canonical element" $$x_U=(y_{\min\{n: x_n\in V_i\}})_{i\in\omega},$$ that is, the $i$th coordinate of our chosen element of $U$ is as small as possible. By construction we have $x_U\in U$. Moreover, since all but finitely many of the $V_i$s are all of $X$, we have $y_i=x_0$ for all but finitely many $i\in\omega$.
But there are only countably many sequences of natural numbers which are eventually all zeroes. This means that the set $$E=\{x_U: U\mbox{ nonempty basic open}\}$$ is countable, regardless of how many basic open sets there are. And since each basic open set contains an element of $E$, the set $E$ is dense in $X^\omega$. So we're done.
(This is exactly the same as the argument above, but with the explicit choice of $D$ as the set of all eventually-zero sequences of natural numbers.)

$^1$Note that it's crucial that we use the product, rather than box, topology here. Of course the $\omega$th box power of a space need not be separable. For example, let $\mathcal{R}$ be the $\omega$th box power of $\mathbb{R}$ with the usual topology, and for each countable set $A=\{(r_i^j)_{i\in\omega}: j\in\omega\}$ of points in $\mathcal {R}$ consider the nonempty $\mathcal{R}$-basic open set $$\prod_{k\in\omega}(r^i_i, r^i_i+1).$$ This is a nonempty open set containing none of the points in $A$.
