[proofplan] The strategy is to construct an explicit $K$-basis for $L$ from a $K$-basis of $M$ and an $M$-basis of $L$. Fix a $K$-basis $\{e_1, \ldots, e_m\}$ of $M$ and an $M$-basis $\{f_1, \ldots, f_n\}$ of $L$, where $m = [M : K]$ and $n = [L : M]$. We show that the $mn$ products $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ form a $K$-basis of $L$ by verifying two properties: (1) every element of $L$ is a $K$-linear combination of the $e_i f_j$ (spanning), and (2) no nontrivial $K$-linear combination of the $e_i f_j$ equals zero (linear independence). The degree formula $[L : K] = mn = [L : M] \cdot [M : K]$ then follows from the cardinality of this basis. [/proofplan]

[step:Fix bases for each layer and expand an arbitrary element of $L$ as a $K$-linear combination of the products $e_i f_j$]Let $m := [M : K]$ and $n := [L : M]$. By hypothesis, both $m$ and $n$ are finite. Fix a $K$-basis $\{e_1, \ldots, e_m\}$ of $M$ and an $M$-basis $\{f_1, \ldots, f_n\}$ of $L$. Let $x \in L$ be arbitrary. Since $\{f_1, \ldots, f_n\}$ is an $M$-basis of $L$, there exist unique coefficients $b_1, \ldots, b_n \in M$ such that \begin{align*} x = \sum_{j=1}^{n} b_j f_j. \end{align*} Each $b_j$ lies in $M$, and $\{e_1, \ldots, e_m\}$ is a $K$-basis of $M$, so for each $j \in \{1, \ldots, n\}$ there exist unique scalars $a_{1j}, \ldots, a_{mj} \in K$ such that \begin{align*} b_j = \sum_{i=1}^{m} a_{ij} \, e_i. \end{align*} Substituting this expansion into the expression for $x$ and applying the distributive law in the field $L$: \begin{align*} x &= \sum_{j=1}^{n} \left(\sum_{i=1}^{m} a_{ij} \, e_i\right) f_j \\ &= \sum_{j=1}^{n} \sum_{i=1}^{m} a_{ij} \, (e_i f_j) \\ &= \sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \, (e_i f_j). \end{align*} The second equality uses that multiplication in $L$ distributes over addition. The interchange of summation order in the third equality is valid because all sums are finite. Since each $a_{ij} \in K$, this expresses $x$ as a $K$-linear combination of the products $\{e_i f_j\}$. Since $x \in L$ was arbitrary, the set $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ spans $L$ as a $K$-vector space.[/step]

[guided]The goal of this step is to show that every element of $L$ can be written as a $K$-linear combination of the $mn$ products $e_i f_j$. The argument proceeds by a double expansion, using a basis at each layer of the tower $K \subset M \subset L$. **First expansion.** Let $x \in L$ be arbitrary. Since $\{f_1, \ldots, f_n\}$ is an $M$-basis of $L$, there exist unique coefficients $b_1, \ldots, b_n \in M$ such that \begin{align*} x = \sum_{j=1}^{n} b_j f_j. \end{align*} At this stage, $x$ is expressed as an $M$-linear combination of the $f_j$. However, the coefficients $b_j$ lie in $M$, not in $K$. To reach a $K$-linear combination, we need to expand each $b_j$ further. **Second expansion.** Each $b_j$ is an element of $M$, and $\{e_1, \ldots, e_m\}$ is a $K$-basis of $M$. Therefore, for each $j \in \{1, \ldots, n\}$, there exist unique scalars $a_{1j}, \ldots, a_{mj} \in K$ such that \begin{align*} b_j = \sum_{i=1}^{m} a_{ij} \, e_i. \end{align*} **Combining the two expansions.** Substituting the second expansion into the first: \begin{align*} x &= \sum_{j=1}^{n} \left(\sum_{i=1}^{m} a_{ij} \, e_i\right) f_j \\ &= \sum_{j=1}^{n} \sum_{i=1}^{m} a_{ij} \, (e_i f_j) \\ &= \sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \, (e_i f_j). \end{align*} Why are these manipulations valid? In the second line, we distribute the multiplication by $f_j$ over the sum $\sum_i a_{ij} \, e_i$. This uses the distributive law in $L$, together with associativity: $a_{ij} \, e_i \, f_j = a_{ij} \cdot (e_i f_j)$. Here $a_{ij} \in K \subset M \subset L$, $e_i \in M \subset L$, and $f_j \in L$, so all products are computed within the field $L$. The interchange of summation order in the third line is justified because both sums are finite. The result is that $x = \sum_{i,j} a_{ij} \, (e_i f_j)$ with all $a_{ij} \in K$. Since $x$ was an arbitrary element of $L$, the set $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ spans $L$ over $K$. This double-expansion technique is the standard method for constructing bases of composite extensions: decompose the problem into two layers and use a basis at each layer. The approach generalises to any finite tower of extensions $K = K_0 \subset K_1 \subset \cdots \subset K_r = L$, yielding the iterated Tower Law $[L : K] = \prod_{s=0}^{r-1} [K_{s+1} : K_s]$.[/guided]

[step:Group a $K$-linear dependence relation by the $M$-basis $\{f_j\}$ and apply independence at both layers]Suppose the products $\{e_i f_j\}$ satisfy a $K$-linear relation: there exist scalars $a_{ij} \in K$ such that \begin{align*} \sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \, (e_i f_j) = 0. \end{align*} We must show that $a_{ij} = 0$ for all $i, j$. Regroup the sum by collecting all terms sharing the same basis element $f_j$: \begin{align*} \sum_{j=1}^{n} \underbrace{\left(\sum_{i=1}^{m} a_{ij} \, e_i\right)}_{=:\, c_j} f_j = 0. \end{align*} For each $j$, the element $c_j := \sum_{i=1}^{m} a_{ij} \, e_i$ lies in $M$, since each $a_{ij} \in K \subset M$ and each $e_i \in M$, and $M$ is closed under addition and scalar multiplication. The equation $\sum_{j=1}^{n} c_j f_j = 0$ is therefore an $M$-linear combination of $\{f_1, \ldots, f_n\}$ equal to zero. Since $\{f_1, \ldots, f_n\}$ is linearly independent over $M$ (being an $M$-basis of $L$), we conclude \begin{align*} c_j = \sum_{i=1}^{m} a_{ij} \, e_i = 0 \quad \text{for every } j \in \{1, \ldots, n\}. \end{align*} Each equation $c_j = 0$ is a $K$-linear combination of $\{e_1, \ldots, e_m\}$ equal to zero. Since $\{e_1, \ldots, e_m\}$ is linearly independent over $K$ (being a $K$-basis of $M$), we conclude \begin{align*} a_{ij} = 0 \quad \text{for every } i \in \{1, \ldots, m\} \text{ and } j \in \{1, \ldots, n\}. \end{align*} Hence the set $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ is linearly independent over $K$.[/step]

[guided]The goal of this step is to show that no nontrivial $K$-linear combination of the products $e_i f_j$ equals zero. The argument applies linear independence at two levels of the tower, in sequence. **Setup.** Suppose there exist scalars $a_{ij} \in K$ (indexed by $1 \le i \le m$, $1 \le j \le n$) such that \begin{align*} \sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \, (e_i f_j) = 0. \end{align*} We want to prove that every $a_{ij}$ is zero. **First layer: exploit independence of the $f_j$ over $M$.** The key idea is to rewrite the left-hand side as an $M$-linear combination of the $f_j$, so that we can invoke their independence over $M$. For each $j$, define \begin{align*} c_j := \sum_{i=1}^{m} a_{ij} \, e_i. \end{align*} Each $c_j$ is an element of $M$: the scalars $a_{ij}$ lie in $K \subset M$, the elements $e_i$ lie in $M$, and $M$ is a field (hence closed under addition and multiplication). Regrouping the double sum by the index $j$: \begin{align*} 0 = \sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \, (e_i f_j) = \sum_{j=1}^{n} \left(\sum_{i=1}^{m} a_{ij} \, e_i\right) f_j = \sum_{j=1}^{n} c_j \, f_j. \end{align*} This is now an $M$-linear combination of $\{f_1, \ldots, f_n\}$ equal to zero. Since $\{f_1, \ldots, f_n\}$ is an $M$-basis of $L$, it is in particular linearly independent over $M$. Therefore $c_j = 0$ for every $j \in \{1, \ldots, n\}$. Why must we argue in this order — first applying independence of the $f_j$ and then of the $e_i$? Because the $f_j$ live in $L$ and are independent over $M$, not over $K$. We cannot directly apply independence of the $e_i$ without first isolating the coefficient of each $f_j$. The regrouping step converts a single relation in $L$ (involving all $mn$ products) into $n$ separate relations in $M$ (each involving only the $m$ elements $e_i$). **Second layer: exploit independence of the $e_i$ over $K$.** For each fixed $j$, the equation $c_j = 0$ reads \begin{align*} \sum_{i=1}^{m} a_{ij} \, e_i = 0 \end{align*} with all $a_{ij} \in K$. This is a $K$-linear combination of $\{e_1, \ldots, e_m\}$ equal to zero. Since $\{e_1, \ldots, e_m\}$ is a $K$-basis of $M$, it is linearly independent over $K$. Therefore $a_{ij} = 0$ for every $i \in \{1, \ldots, m\}$. Since this holds for every $j \in \{1, \ldots, n\}$, we have $a_{ij} = 0$ for all $i$ and $j$. The set $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ is therefore linearly independent over $K$. The structure of this argument — group by one basis, apply independence, then apply independence of the other basis — is characteristic of proofs involving iterated extensions. It mirrors the spanning argument in the previous step, but runs "in reverse": the spanning argument builds up a representation (expand in the $f_j$, then expand each coefficient in the $e_i$), while the independence argument tears one down (group by the $f_j$, force their coefficients to vanish, then force each coefficient's components to vanish).[/guided]

[step:Conclude that $\{e_i f_j\}$ is a $K$-basis of $L$ and read off the degree formula] The preceding two steps establish that the set $\{e_i f_j : 1 \le i \le m, \, 1 \le j \le n\}$ spans $L$ over $K$ and is linearly independent over $K$. Therefore it is a $K$-basis of $L$. This basis contains exactly $m \cdot n$ elements, so $[L : K] = mn$. Substituting $m = [M : K]$ and $n = [L : M]$: \begin{align*} [L : K] = [L : M] \cdot [M : K]. \end{align*} In particular, since $m$ and $n$ are both finite, $[L : K] = mn$ is finite. [/step]