The Stacks project

Proof. This is a corollary of Lemma 9.12.10. Namely, since $K/F$ is finite we can find finitely many elements $\alpha _1, \ldots , \alpha _ n \in K$ generating $K$ over $F$ (for example we can choose the $\alpha _ i$ to be a basis of $K$ over $F$). If $K/F$ is separable, then each $\alpha _ i$ is separable over $F(\alpha _1, \ldots , \alpha _{i - 1})$ by Lemma 9.12.3 and we get equality by Lemma 9.12.10. On the other hand, if we have equality, then no matter how we choose $\alpha _1, \ldots , \alpha _ n$ we get that $\alpha _1$ is separable over $F$ by Lemma 9.12.10. Since we can start the sequence with an arbitrary element of $K$ it follows that $K$ is separable over $F$. $\square$