Density of $Y = \left\lbrace f \in [0,1]^{[0,1]} : \operatorname{supp}(f) \leq \left\lvert \mathbb{N} \right\rvert \right\rbrace$ I'd like to prove that given $X = [0,1]^{[0,1]}$ has a subspace, which is indeed $Y$, that is sequentially compact but not compact. To prove that I need to prove that $Y$ is dense in $X$, where I denote $\operatorname{supp}(f) = \left\lbrace x \in [0,1] : f(x) \ne 0 \right\rbrace$.
My effort : given $Y = \left\lbrace f \in X : \operatorname{supp}(f) \leq \left\lvert \mathbb{N} \right\rvert \right\rbrace$ it is sufficient to prove that $Y \cap U \ne \emptyset$ just for $U$ of the form $U = \prod\limits_{t \in [0,1]} U_{t}$ where $U_{t} \ne [0,1]$ just for finite $t \in [0,1]$. Then if $f(t) = \hspace{0.1cm} \begin{cases} 0 & U_{t} = [0,1] \\ a \in [0,1] & U_{t} \ne [0,1]\end{cases}$
But I'm not sure if I can conclude that $f \in U \cap Y$ which implies my thesis.
Any help or hint would be appreciated.
 A: You definition for $f$ is close to correct but not quite. We have to chose a (posssibly different) $a_t \in U_t$ for each of the finitely many $U_t$ that are not $[0,1]$ (now, it looks like you pick any fixed and arbitrary $a$ for all these coordinates, which is not what you want). This can be done as all $U_t$ are non-empty (or $U$ would be empty, and we show denseness by finding $f \in U \cap Y$ for each non-empty basic open $U$.
So having these (finitely many so AC-friendly) choices $a_t \in U_t$ define
$$f = \begin{cases}
0 & \text{ if } U_t = [0,1]\\
a_t & \text{ otherwise}\\
\end{cases}$$
and $\operatorname{supp}(f)$ is finite, namely the finitely many coordinates of the $a_t$, and so $f \in Y$ and $f \in U$ is by construction of $f$.
So $Y$ is a dense subspace of $X=[0,1]^{[0,1]}$ and is called the $\Sigma$-product (wrt the $0$-function) of continuum many copies of $[0,1]$. (The functions with finite support are called the $\sigma$-product, and is also dense).
If $A \subseteq Y$ is a countable subset, then we consider
$$S = \bigcup \{\operatorname{supp}(f): f \in A\}$$
and $S$ is a countable union of countable sets, so a countable subset of $[0,1]$. Then $\pi_S: Y \to Z:=[0,1]^S$ defined by $\pi_S(f)=f\restriction_S$ is continuous (basically a projection onto a subproduct, restricted to $Y$), and $A'=\pi_S[A]$ is a countable subset in the compact metrisable space $Z$. So $A'$ has an accumulation point $g$ in $Z$ and padding $g$ with $0$ outside $S$ we get a function $\hat{g} \in Y$ that is an accumulation point of $A$ in $Y$ (check this!).
Similarly, if $A$ had been the image set of a sequence $(f_n)_n$ in $Y$, then $(\pi_S(f_n))_n$ has a convergent subsequence with limit $g$ and its "padded version" $\hat{g} \in Y$ is the limit of the "same" subsequence in $Y$. This uses that in the metrisable $Z$, we do have that sequential compactness, compactness etc. coincide.
So $Y$ is a sequentially compact subset of $X$ (which is not sequentially compact) that is not closed, but even dense. And $X$ is countably compact (and normal and what all) but its countably compact subspace $Y$ is not closed in it. A nice contrast with the situation for compact spaces (where in Hausdorff spaces compact subspaces are always closed).
