Proof of Theorem OBNM

Let $U$ be the unitary matrix promised by Theorem OD and let $D$ be the resulting diagonal matrix. The desired set of vectors is formed by collecting the columns of $U$ into a set. Theorem CUMOS says this set of columns is orthonormal. Since $U$ is nonsingular (Theorem UMI), Theorem CNMB says the set is a basis.

Since $A$ is diagonalized by $U$, the diagonal entries of the matrix $D$ are the eigenvalues of $A$. An argument exactly like the second half of the proof of Theorem DC shows that each vector of the basis is an eigenvector of $A$.