Solution (source code)

= Solution

Since $K$ is an $F$-<vector subspace> of the finite-dimensional <vector space> $L$, it has a finite $F$-<basis> $u_1,\ldots,u_m$. Any finite $F$-spanning set for $L$ also spans $L$ over $K$, so choose a finite $K$-<basis> $v_1,\ldots,v_r$ of $L$.

Every $\ell\in L$ can be expanded first in the $v_j$ and then in the $u_i$, showing that the products $u_i v_j$ span $L$ over $F$. If $\sum_{i,j}c_{ij}u_i v_j=0$ with $c_{ij}\in F$, <independence> of the $v_j$ over $K$ gives $\sum_i c_{ij}u_i=0$ for every $j$; <independence> of the $u_i$ then gives every $c_{ij}=0$. The products form an $F$-<basis>, proving the <tower law for field extensions>:
$$
\boxed{[L:F]=rm=[L:K][K:F]}.
$$