The norm completion of an inner-product space is a Hilbert space

Let $\xi ,\eta \in \widehat{X}$. For every $n$, density makes the sets $\{x\in X:\mathrm{\parallel }\kappa x-\xi \mathrm{\parallel }<1\mathrm{/}(n+1)\}$ and $\{y\in X:\mathrm{\parallel }\kappa y-\eta \mathrm{\parallel }<1\mathrm{/}(n+1)\}$ nonempty. Countable Choice selects $x_n,y_n$ from these sets. Thus $\kappa (x_n)\to \xi$ and $\kappa (y_n)\to \eta$, the selected sequences are Cauchy, and continuity of the vector operations gives $\kappa (x_n\pm y_n)=\kappa (x_n)\pm \kappa (y_n)\to \xi \pm \eta$.

The parallelogram identities $\mathrm{\parallel }{x}_n+y_n{\mathrm{\parallel }}^2+\mathrm{\parallel }{x}_n-y_n{\mathrm{\parallel }}^2=2\mathrm{\parallel }{x}_n{\mathrm{\parallel }}^2+2\mathrm{\parallel }{y}_n{\mathrm{\parallel }}^2$ hold in $X$ by [A6]; passing to the limit using continuity of the norm and of sums, and the isometry $\mathrm{\parallel }\kappa z\mathrm{\parallel }=\mathrm{\parallel }z\mathrm{\parallel }$, gives $\mathrm{\parallel }\xi +\eta {\mathrm{\parallel }}^2+\mathrm{\parallel }\xi -\eta {\mathrm{\parallel }}^2=2\mathrm{\parallel }\xi {\mathrm{\parallel }}^2+2\mathrm{\parallel }\eta {\mathrm{\parallel }}^2$, so the completion norm satisfies the parallelogram law.

The Jordan–von Neumann theorem applied to the Banach space $\widehat{X}$ therefore produces an inner product $B$ on $\widehat{X}$ whose induced length is exactly the completion norm and which is the unique such inner product.

$B$ extends the original pairing: for $x,y\in X$, the polarisation formula of [A2] together with $\kappa (x\pm y)=\kappa x\pm \kappa y$ and the isometry property gives $B(\kappa x,\kappa y)=\frac{1}{4}(\mathrm{\parallel }\kappa (x+y){\mathrm{\parallel }}^2-\mathrm{\parallel }\kappa (x-y){\mathrm{\parallel }}^2)=\frac{1}{4}(\mathrm{\parallel }x+y{\mathrm{\parallel }}^2-\mathrm{\parallel }x-y{\mathrm{\parallel }}^2)=⟨x,y⟩$ in the real case, and the four-term complex formula likewise in the complex case.

Uniqueness: if $B^{\mathrm{\prime }}$ is any inner product on $\widehat{X}$ that extends the pairing along $\kappa$ and induces the completion norm, then for $\xi ,\eta$ and approximating sequences as in step 1.1 the Cauchy–Schwarz inequality for both forms gives $\mathrm{\mid }{B}^{\mathrm{\prime }}(\xi ,\eta )-B^{\mathrm{\prime }}(\kappa x_n,\kappa y_n)\mathrm{\mid }\le \mathrm{\parallel }\xi -\kappa x_n\mathrm{\parallel }\mathrm{\parallel }\eta \mathrm{\parallel }+\mathrm{\parallel }\kappa x_n\mathrm{\parallel }\mathrm{\parallel }\eta -\kappa y_n\mathrm{\parallel }$ and the same bound for $B$, so both pairings are the limits of the common values $⟨x_n,y_n⟩$ and $B^{\mathrm{\prime }}=B$.

Hence $\widehat{X}$ carries the inner product $B$ extending the original one with the completion norm as induced length, so it is complete and therefore a Hilbert space by [A7]. Countable Choice is used in the published completion interface and explicitly in step 1.1 to select the two approximating sequences; no further choice enters the limit arguments.