Let $V$ be a finite dimensional vector space of complex valued functions, polynomials, say. Suppose $V$ is closed under the usual complex conjugation $\overline{V}=V$.
Can we take an orthonormal basis consisting of real-valued functions?
Work:
Let $\{v_1,\dots,v_n\}$ be an orthonormal basis. Then, so $\{\overline{v_1},\dots,\overline{v_n}\}$ is.
It does not have to be explicit, but $\{w_i:=c(v_i+\overline{v_i})\}_{i=1,\dots,n}$ for some $c\in\mathbb{R}$ would be a reasonable guess, but cannot show the orthonormalness. (If I can start from that a real orthonormal system $\{w_i\}$ is given I can construct a complex one, but I don't know if I can do the other way around).