Solution (source code)

= Solution

Since $K\subseteq L$ and $L/F$ is finite, an $F$-<linearly independent> set in $K$ remains independent in $L$, so $K/F$ is finite. A finite $F$-spanning set of $L$ also spans it over $K$, so $L/K$ is finite.

Take an $F$-<basis> $a_1,\ldots,a_m$ of $K$ and a $K$-<basis> $b_1,\ldots,b_n$ of $L$. Expanding coefficients twice shows that all products $a_ib_j$ span $L$ over $F$. If $\sum_{i,j}c_{ij}a_ib_j=0$ with $c_{ij}\in F$, independence of the $b_j$ forces $\sum_ic_{ij}a_i=0$ for each $j$, and then independence of the $a_i$ forces every coefficient zero. Thus these products form an $F$-<basis>, proving
$$
\boxed{[L:F]=[L:K][K:F].}
$$