Solution (source code)

= Solution

As written, the assertion needs a \b[nonzero-vector assumption]: the singleton set containing the <zero vector> is mutually orthogonal but is <linearly dependent>. For the <linear independence of nonzero orthogonal vectors>, suppose $\sum_{i=1}^k\alpha_iq_i=0$. Taking the <inner product> with $q_j$ gives
$$
0=\sum_i\alpha_i\langle q_i,q_j\rangle=\alpha_j\lVert q_j\rVert^2.
$$
Since $q_j\ne0$, positive definiteness gives $\lVert q_j\rVert^2>0$, hence $\alpha_j=0$. This holds for every $j$, proving <linear independence> under the necessary assumption.