A bounded sequence in a separable Hilbert space has a weakly convergent subsequence

By separability choose a dense subset $D\subseteq H$ that is at most countable. It is nonempty because $H$ contains $0$. If $D$ is finite, a finite listing from its bijection with a natural number, repeated periodically, gives a sequence; if $D$ is countably infinite, a bijection with $\mathbb{N}$ gives a sequence. Thus [F4] supplies a dense sequence $(v_j{)}_{j\ge 1}$ without any choice principle beyond the witnesses in the definition of countability.

For any bounded real sequence $(a_k)$ in $[-R,R]$, start with $I_0=[-R,R]$. At each stage split the current interval into its two closed halves and choose the left half if it contains infinitely many terms of the current sequence, and otherwise choose the right half. At least one half contains infinitely many terms. Choose the least index later than the preceding selected index whose term lies in the chosen half. The resulting nested intervals have lengths tending to zero, so [F1] gives a common point, and the selected subsequence converges to it. Every choice in this construction is the least natural index or the leftmost of two alternatives, so the extraction is determined by its input sequence.

For each $j$, the scalar sequence $⟨x_n,v_j{⟩}_H$ is bounded by $C\mathrm{\parallel }{v}_j{\mathrm{\parallel }}_H$ by [F3]. Apply the deterministic extraction in step 1.2 successively to these coordinate sequences, each time inside the previously obtained subsequence. This recursive rule produces nested infinite subsequences $N_1\supseteq N_2\supseteq \cdots$ on which the first, first two, and then first $j$ pairings converge, respectively. Let $n_k$ be the $k$th index of $N_k$. Nestedness makes $(n_k)$ strictly increasing, and for each fixed $j$ the sequence $⟨x_{n_k},v_j{⟩}_H$ converges because its tail is a subsequence of $N_j$.

For any $v\in H$, choose $v_j$ arbitrarily close to $v$. For indices $k,\mathrm{\ell }$, [F3] gives $\mathrm{\mid }⟨x_{n_k}-x_{n_{\mathrm{\ell }}},v{⟩}_H\mathrm{\mid }\le \mathrm{\mid }⟨x_{n_k}-x_{n_{\mathrm{\ell }}},v_j{⟩}_H\mathrm{\mid }+2C\mathrm{\parallel }v-v_j{\mathrm{\parallel }}_H\mathrm{.}$ The first term tends to zero as $k,\mathrm{\ell }\to \mathrm{\infty }$ for fixed $j$, and the second can be made arbitrarily small by density. Thus $⟨x_{n_k},v{⟩}_H$ converges for every $v$. Its limit $L(v)$ is linear and satisfies $\mathrm{\mid }L(v)\mathrm{\mid }\le C\mathrm{\parallel }v{\mathrm{\parallel }}_H$, so $L$ is a bounded linear functional. By [F2] there is a unique $x\in H$ with $L(v)=⟨x,v{⟩}_H$ for all $v$. Therefore $x_{n_k}\rightharpoonup x$.