Solution (source code)

= Solution

For $a_n=\langle x,e_n\rangle$, the finite <orthogonal projection> $P_Nx=\sum_{|n|\leq N}a_ne_n$ satisfies
$$
0\leq\|x-P_Nx\|^2=\|x\|^2-\sum_{|n|\leq N}|a_n|^2.
$$
This is <Bessel's inequality>, so the coefficients are square summable. The preceding result gives a limit $s=\sum_na_ne_n$. For each fixed $k$, <continuity> of the <inner product> gives $\langle x-s,e_k\rangle=0$. The <completeness> assumption on the <orthonormal system> forces $x-s=0$. Hence
$$
\boxed{x=\sum_{n\in\mathbb Z}\langle x,e_n\rangle e_n.}
$$
Taking squared norms also gives <Parseval's identity>, $\|x\|^2=\sum_n|\langle x,e_n\rangle|^2$.