real analysis – Proof of (ii)$implies$ (iii) in Theorem $4.18$, Rudin’s RCA

Rudin says that (ii)$implies$(iii) of Theorem $4.18$ follows from Theorem $4.17$. I do not see how, although I have tried two different approaches. I have described my work below and attached the theorems for reference below at the end of the post.


Approach 1: Assume (ii), i.e. $P$ is dense in $H$. Then for every $epsilon > 0$ and $xin H$, there exists a finite $Fsubset A$ and $c_alpha$‘s such that $$left|x – sum_{alpha in F} c_alpha u_alpharight| < epsilon$$
We have $sum_{alphain A} |hat x(alpha)|^2 le |x|^2$ from Theorem $4.17$ already. If we can show $sum_{alphain A} |hat x(alpha)|^2 ge |x|^2$, we are done. I observed that
$$|x| le left|x – sum_{alpha in F} c_alpha u_alpharight| + left|sum_{alphain F}c_alpha u_alpha right| < epsilon + sum_{alphain F}|c_alpha|^2$$
which doesn’t really help.

Approach 2: The proof of Theorem $4.17$ says that $f$ is an isometry of $P$ onto the dense subspace of $ell^2(A)$ consisting of finitely supported functions. Since we assume $P$ is dense in $H$, there is a sequence $(x_n)$ of elements in $P$, such that $x_nto xin H$. Since $0in P$ and $f$ is an isometry of $P$, we see that
$$|x_n|^2 = |f(x_n)|^2$$
$$|x_n|^2 = |hat x_n|^2 = sum_{alphain A}|hat x_n(alpha)|^2$$
Taking limits,
$$lim_{ntoinfty}|x_n|^2 = lim_{ntoinfty} sum_{alphain A}|hat x_n(alpha)|^2$$
Rudin defines $sum_{alphain A} phi(alpha)$ as $sup_{Fsubset A, |F| < infty} sum_{alphain F}phi(alpha)$ where $F$ is a finite subset of $A$, i.e. we take supremum over all finite sums.
Then,
$$lim_{ntoinfty}|x_n|^2 = lim_{ntoinfty} sup_{Fsubset A} sum_{alphain F, |F| < infty}|hat x_n(alpha)|^2$$
If we can switch $lim$ and $sup$ in the expression above, we are essentially done – but I’m not sure if the swapping is allowed.


Attached for reference:
Theorem 4.18:
enter image description here
Theorem 4.17:
enter image description here

Thank you!