Corollary
Tag 07ZQ, permanent. Cite it as [Bourbaki, Tag 07ZQ].
Topological Vector Spaces, V, p. 24, § 2. Orthogonal families in a hilbertian space
In every Hausdorff prehilbertian space E satisfying the first axiom of countability, there exists a countable orthonormal basis.
If E satisfies the first axiom of countability, then there exists a total sequence in E, and we can always extract an independent total family from such a sequence (A, II, § 7, No. 1, th. 2).
We can give examples of Hausdorff prehilbertian spaces not having any orthonormal basis (V, p. 70, exerc. 2).
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.
Cited by
Nothing.