Proof of The Computational Basis and the State Vectors of a Qubit

Here $n=2$, so by the base clause and the recursion of Finite Sum Notation in a Field every sum below has the form $\sum_{k=1}^{2}a_{k}=a_{1}+a_{2}$. Components and operations are those of The Complex Coordinate Space, the inner product is that of Standard Inner Product on the Complex Coordinate Space, which is an inner product by The Standard Inner Product Makes the Complex Coordinate Space an Inner Product Space, and $\lVert\cdot\rVert$ is the induced norm. By claim 1 of Properties of Complex Conjugation and Modulus the conjugates of the real numbers $0$ and $1$ are $0$ and $1$ themselves.

Claim 1. Computing directly from the definition of the standard inner product, and using $0\cdot z=0$ and $1z=z$ in the field of complex numbers,

Moreover $\lVert e_{1}\rVert^{2}=\langle e_{1},e_{1}\rangle=1$ and $0\le\lVert e_{1}\rVert$; since $1$ is also nonnegative with square $1$, Existence and Uniqueness of the Nonnegative Square Root gives $\lVert e_{1}\rVert=1$, so $e_{1}$ is a unit vector, and likewise $e_{2}$.

Claim 2. $\langle e_{1},u\rangle=\overline{1}\,u_{1}+\overline{0}\,u_{2}=u_{1}$ and $\langle e_{2},u\rangle=\overline{0}\,u_{1}+\overline{1}\,u_{2}=u_{2}$.

Claim 3. By the componentwise scalar multiplication, $u_{1}e_{1}=(u_{1}\cdot1,\;u_{1}\cdot0)=(u_{1},0)$ and $u_{2}e_{2}=(0,u_{2})$, so by componentwise addition

If $\alpha,\beta$ are complex numbers with $u=\alpha e_{1}+\beta e_{2}$, then the same computation gives $\alpha e_{1}+\beta e_{2}=(\alpha,\beta)$, and two ordered pairs are equal exactly when their components agree, so $\alpha=u_{1}$ and $\beta=u_{2}$.

Claim 4. By claim 2 of The Standard Inner Product Makes the Complex Coordinate Space an Inner Product Space and the form of sums with $n=2$, $\lVert u\rVert^{2}=|u_{1}|^{2}+|u_{2}|^{2}$. If $u$ is a qubit state vector, that is a unit vector, then $\lVert u\rVert=1$ and hence $|u_{1}|^{2}+|u_{2}|^{2}=\lVert u\rVert^{2}=1$. Conversely, if $|u_{1}|^{2}+|u_{2}|^{2}=1$, then $\lVert u\rVert^{2}=1$ with $0\le\lVert u\rVert$, so $\lVert u\rVert=1$ by Existence and Uniqueness of the Nonnegative Square Root, and $u$ is a qubit state vector in the sense of Qubit State Space.