The answers in the comments are somewhat misleading in two respects.
For one, they don't mention that they use the facts that a) the space of sequences in a metric space is metrizable and b) compactness and sequential compactness are equivalent in metrizable spaces. The desired result can only be proved from Tychonoff's theorem using these facts; the product of an uncountable number of compact metric spaces is in general not metrizable and not sequentially compact.
But more importantly, they obscure the set-theoretic premises required for the desired result. Tychonoff's theorem in full generality is equivalent to the axiom of choice. We're only dealing with a countable product here, but I believe Tychonoff's theorem for countable products still requires the boolean prime ideal theorem and the axiom of countable choice (see this article, p. 2). By contrast, the diagonal argument the OP was looking for requires no choice (not even countable choice):
Given a sequence $s$ of sequences in $X$, denote by $s_i(n)$ the $n$-th element of the $i$-th sequence of $s$. (If you tend to get as confused about such things as I do, it helps to keep in mind the concrete example where $s_i(n)$ is the $n$-th digit in the binary representation of $i$.) Consider the sequence $s_i(1)$ in $X$. Since $X$ is a compact metric space and hence sequentially compact, this sequence contains a convergent subsequence $s_{i_1(k)}(1)$. Denote its limit by $a (1)$. Then consider the sequence $s_{i_1(k)}(2)$ (a subsequence of the sequence $s_i(2)$ in $X$). This sequence, too, has a convergent subsequence $s_{i_2(k)}(2)$ with limit $a (2)$. We can continue this construction for all $n$. Now consider $s_{i_l(l)}$, which is a subsequence of the sequence $s$ of sequences. We can show that it converges against the sequence $a$ of the limits $a (n)$.
An element of the basis of the product topology containing $a$ is a product of factors, only a finite number of which differ from $X$. For each $n$, apart from the first $n$ elements the sequence $s_{i_l(l)}(n)$ is a subsequence of $s_{i_n(l)}(n)$, and thus it is a convergent subsequence of $s_i(n)$ with limit $a (n)$, which will eventually end up in the $n$-th factor of the basis element. Since there are finitely many of these factors, eventually all these convergent subsequences will have ended up in their corresponding factors, so that the entire sequence eventually ends up in the given basis element.
[Edit in response to comments by Nate and Theo:]
Here's a construction that picks a particular convergent subsequence of a sequence having at least one convergent subsequence in a metric space without making arbitrary choices (in case Nate and Theo are right that that requires the axiom of choice):
For a given sequence $b_n$, consider the (non-empty) set of all convergent subsequences for which $\lvert b_n - b \rvert < 2^{-n}$ for all $n$, where $b$ is the limit of the subsequence, and take the least of these subsequences in lexicographical order. We can't just take the lexicographically least convergent subsequence because there isn't one, but we can explicitly construct the lexicographically least convergent subsequence that fulfills the given condition: For each element, just pick the earliest element in the sequence such that the resulting partial subsequence is a prefix of at least one subsequence that fulfills the condition. The result is a Cauchy sequence, and hence, since $X$ is compact, converges. (The same construction doesn't work without the additional condition, since the resulting subsequence would just be the sequence itself.)
So it appears that we can avoid choice. However, that would seem to allow us to reason as follows: The fact that all factors in the product are $X$ was not used. Thus, the result generalizes to arbitrary countable products of compact metric spaces. A countable product of metric spaces is metrizable, and in a metrizable space compactness and sequential compactness are equivalent; thus we've proved that the countable product of compact metric spaces is compact. But now we can plug that into the proof of the equivalence of the axiom of choice and Tychonoff's theorem (linked to above). Since to any compact metric space we can add an isolated point and still have a compact metric space (by limiting the metric to $1$ and choosing a uniform distance to the new point $>1$), this seems to prove the possibility of choice from a countable product of compact metric spaces. This is not the full axiom of countable choice, but it does allow considerable choices that I would have expected to be independent of ZF. Is this true, or is there another fallacy somewhere?
Best Answer
$\{0,1\}^{\mathbb{R}}$ is weakly sequentially compact (it's even compact Hausdorff which implies that property), but it has sequences without convergent subsequences.
$\beta \omega$, the Cech-Stone compactification of the countable discrete space $\omega$ is another example, for the same reasons. The sequence $x_n = n \in \omega$ is a sequence without a convergent subsequence.
"Weakly sequentially compact" is a confusing name IMHO, just call it countably compact (every countable open cover has a finite subcover), to which it is equivalent. I show this fact in my answer here.