Weakly convergent sequences are norm bounded

For every $g\in X^{\ast }$, the scalar sequence $g(x_n)$ converges to $g(x)$, hence is bounded: a tail has modulus at most $\mathrm{\mid }g(x)\mathrm{\mid }+1$, and finitely many preceding moduli have a finite maximum. The maps $J_X{x}_n:X^{\ast }\to \mathbb{K}$ are therefore pointwise bounded bounded linear maps. Their domain $X^{\ast }=\mathcal{B}(X,\mathbb{K})$ is Banach since $\mathbb{K}$ is complete.

Sequential uniform boundedness applied to these maps gives ${\sup }_n\mathrm{\parallel }{J}_X{x}_n\mathrm{\parallel }<\mathrm{\infty }$. The HB isometry makes this ${\sup }_n\mathrm{\parallel }{x}_n\mathrm{\parallel }<\mathrm{\infty }$. Countable Choice is used exactly in F4; HB is used only in F2, and completeness of $X$ was not required.

For the second assertion, each scalar sequence $f_n(y)$ converges for fixed $y\in X$, so the same finite-head/tail estimate from step 1.1 gives pointwise boundedness. Apply F4 directly on the assumed Banach domain $X$ to obtain ${\sup }_n\mathrm{\parallel }{f}_n\mathrm{\parallel }<\mathrm{\infty }$. No bidual norming or HB is used in this case. If either domain is zero, all its operator norms are zero, so the same conclusions hold. $\mathrm{\square }$