Suppose X is an inner product space, with Hilbert space completion H (actually, I'm interested in the *real* scalar case, but I doubt there's any difference). If H is separable, then so is X, and I can find a (countable or finite) orthonormal basis of H inside X. Indeed, start with some countable subset Y of X which is dense in H. Then, by induction, we can move to a linearly independent subset of Y, and then apply Gram–Schmidt, again by induction. The point (to me, anyway) is that at any stage, we never take limits, and so we never leave X.

Now, what happens if H is not assumed separable? I've tried to use a Zorn's Lemma argument, but I keep end up wanting to take limits (or, rather, infinite sums) which gives me an orthonormal basis (in the generalised, non-countable, sense) in H, but I cannot ensure that it's in X. Am I just missing something obvious, or is there a slight technicality here...?