[proofplan]
We regard field extensions as vector spaces and prove the degree formula directly from bases. First, because $K$ is finite-dimensional over $k$, the intermediate field $L$ is a finite-dimensional $k$-subspace of $K$. Next, a finite $k$-spanning set for $K$ also spans $K$ over $L$, so $K / L$ is finite. Finally, choosing a $k$-basis of $L$ and an $L$-basis of $K$, we show that all products of basis elements form a $k$-basis of $K$, giving $[K : k] = [K : L][L : k]$ and the divisibility statement.
[/proofplan]
[step:Show that the intermediate field is finite over the base field]
Let $N := [K : k]$. Since $K / k$ is finite, $N \in \mathbb{N}$ and $K$ is an $N$-dimensional [vector space](/page/Vector%20Space) over $k$.
Because $k \subset L \subset K$, the field $L$ is closed under addition and scalar multiplication by elements of $k$. Thus $L$ is a $k$-vector subspace of the finite-dimensional $k$-vector space $K$. Every $k$-linearly independent family in $L$ is also $k$-linearly independent in $K$, so its length is at most $N$. Hence $L$ is finite-dimensional over $k$.
Define
\begin{align*}
m := [L : k].
\end{align*}
Then $m \in \mathbb{N}$, and there exists a $k$-basis $(\ell_1, \dots, \ell_m)$ of $L$.
[/step]
[step:Show that the top field is finite over the intermediate field]
Let $(u_1, \dots, u_N)$ be a $k$-basis of $K$. For each $x \in K$, there are coefficients $a_1, \dots, a_N \in k$ such that
\begin{align*}
x = \sum_{r=1}^{N} a_r u_r.
\end{align*}
Since $k \subset L$, the same coefficients satisfy $a_1, \dots, a_N \in L$. Therefore $(u_1, \dots, u_N)$ spans $K$ as a vector space over $L$.
Thus $K$ is finite-dimensional over $L$. Define
\begin{align*}
n := [K : L].
\end{align*}
Then $n \in \mathbb{N}$, and there exists an $L$-basis $(v_1, \dots, v_n)$ of $K$.
[guided]
The point of this step is to verify that the degree $[K : L]$ is a finite integer before we use it in a product formula. We start with the given finite extension $K / k$, so there is a $k$-basis $(u_1, \dots, u_N)$ of $K$, where $N := [K : k]$.
Take any element $x \in K$. Since $(u_1, \dots, u_N)$ spans $K$ over $k$, there are scalars $a_1, \dots, a_N \in k$ such that
\begin{align*}
x = \sum_{r=1}^{N} a_r u_r.
\end{align*}
But the inclusion $k \subset L$ says that every scalar from $k$ is also a scalar from $L$. Therefore the same expression is an $L$-linear combination of $u_1, \dots, u_N$. This proves that $(u_1, \dots, u_N)$ spans $K$ over $L$.
A vector space with a finite spanning set is finite-dimensional. Hence $K$ is finite-dimensional over $L$, so
\begin{align*}
n := [K : L]
\end{align*}
is a positive integer. We may therefore choose an $L$-basis $(v_1, \dots, v_n)$ of $K$.
[/guided]
[/step]
[step:Construct a $k$-basis of $K$ from the two smaller bases]
We claim that the family
\begin{align*}
\mathcal{B} := \{\ell_i v_j : 1 \leq i \leq m,\ 1 \leq j \leq n\}
\end{align*}
is a $k$-basis of $K$.
First, we prove spanning. Let $x \in K$. Since $(v_1, \dots, v_n)$ is an $L$-basis of $K$, there are coefficients $c_1, \dots, c_n \in L$ such that
\begin{align*}
x = \sum_{j=1}^{n} c_j v_j.
\end{align*}
Since $(\ell_1, \dots, \ell_m)$ is a $k$-basis of $L$, for each $j \in \{1, \dots, n\}$ there are coefficients $a_{1j}, \dots, a_{mj} \in k$ such that
\begin{align*}
c_j = \sum_{i=1}^{m} a_{ij}\ell_i.
\end{align*}
Substituting these expressions into the expansion of $x$ gives
\begin{align*}
x = \sum_{j=1}^{n}\left(\sum_{i=1}^{m} a_{ij}\ell_i\right)v_j.
\end{align*}
Using distributivity in the field $K$, this becomes
\begin{align*}
x = \sum_{j=1}^{n}\sum_{i=1}^{m} a_{ij}(\ell_i v_j).
\end{align*}
Thus $\mathcal{B}$ spans $K$ over $k$.
Second, we prove $k$-[linear independence](/page/Linear%20Independence). Suppose coefficients $a_{ij} \in k$, indexed by $1 \leq i \leq m$ and $1 \leq j \leq n$, satisfy
\begin{align*}
\sum_{j=1}^{n}\sum_{i=1}^{m} a_{ij}(\ell_i v_j) = 0.
\end{align*}
For each $j \in \{1, \dots, n\}$, define
\begin{align*}
c_j := \sum_{i=1}^{m} a_{ij}\ell_i \in L.
\end{align*}
Then the displayed equality becomes
\begin{align*}
\sum_{j=1}^{n} c_j v_j = 0.
\end{align*}
Since $(v_1, \dots, v_n)$ is $L$-linearly independent, each $c_j = 0$. For each fixed $j$, the equality
\begin{align*}
\sum_{i=1}^{m} a_{ij}\ell_i = 0
\end{align*}
and the $k$-linear independence of $(\ell_1, \dots, \ell_m)$ imply $a_{ij} = 0$ for every $i$. Hence all coefficients $a_{ij}$ are zero, so $\mathcal{B}$ is $k$-linearly independent.
Therefore $\mathcal{B}$ is a $k$-basis of $K$.
[/step]
[step:Count the product basis and obtain the divisibility formula]
The basis $\mathcal{B}$ contains exactly $mn$ elements, one for each ordered pair $(i,j)$ with $1 \leq i \leq m$ and $1 \leq j \leq n$. Since $\mathcal{B}$ is a $k$-basis of $K$,
\begin{align*}
[K : k] = mn.
\end{align*}
By the definitions of $m$ and $n$, this is
\begin{align*}
[K : k] = [L : k][K : L].
\end{align*}
Since $[K : L] \in \mathbb{N}$, the integer $[L : k]$ divides the integer $[K : k]$. Rearranging the same equality gives
\begin{align*}
[K : L] = \frac{[K : k]}{[L : k]}.
\end{align*}
This proves both assertions.
[/step]
