Solution (source code)

= Solution

A set is <linearly dependent> if some finite selection of distinct vectors admits a relation $\sum_jc_jv_j=0$ with coefficients not all zero. For a finite set this is just such a nontrivial relation using its vectors.

Prove dependence of $n+1$ vectors in $\mathbb R^n$ by induction, starting with the zero-dimensional case. If all first coordinates vanish, select $n$ of the vectors and apply induction in $\mathbb R^{n-1}$. Otherwise relabel so the last vector has first coordinate $a\ne0$. For $1\leq j\leq n$, put $w_j=v_j-(v_{j,1}/a)v_{n+1}$. These $n$ vectors have zero first coordinate, so induction supplies $\sum_{j=1}^nc_jw_j=0$, with some $c_j\ne0$. Expanding gives a nontrivial <linear dependence> among the original vectors. The same proof works over any <field>.

Now express vectors of $V$ in coordinates relative to its given $n$-element <basis>. Any other <basis> has at most $n$ elements: more would contain $n+1$ <linearly dependent> vectors. If it has $m<n$ elements, expressing the original <basis> in its coordinates makes the original $n$ vectors <linearly dependent>, a contradiction. Thus \b[every <basis> has exactly $n$ elements].

Finally, the functions $\sin(jx)$, $j=1,2,\ldots$, are bounded and continuous. Any finite relation among them can be multiplied by $\sin(rx)$ and integrated over $[0,2\pi]$. The <orthogonality> identity
$$
\int_0^{2\pi}\sin(jx)\sin(rx)\,dx=\pi\,\delta_{jr}
$$
forces every coefficient to vanish. Arbitrarily large <linearly independent> finite sets exist, so \b[the <vector space> of bounded continuous functions is infinite-dimensional].