We prove by induction on $[K : F]$.

Trivial case: $[K : F] = 1$. In this case, $K = F$, the proposition is obviously true.

Assume the statement holds for all field extensions of degree $\leq n - 1$. Given a field extension $K / F$ with $[K : F] = n$, take $\alpha \in K - F$, by Proposition 17010, $$ \begin{align*} &\# \{ F\text{- embeddings } \varphi : K \to \overline{F} \} \\ = &\# \{ F\text{-embeddings } \varphi : F(\alpha) \to \overline{F} \} \cdot \#\{ F(\alpha)\text{-embeddings }\varphi : K \to \overline{F(\alpha)} = \overline{F} \}. \end{align*} $$ By Proposition 1709, $$ \#\{ F\text{-embeddings }\varphi : F(\alpha) \to \overline{F} \} = \# \{ \text{roots of }m_{\alpha, F}(x) \text{ in }\overline{F} \} \leq [F(\alpha) : F] $$ $[K : F(\alpha)] < n$, so by the induction hypothesis, $$ \# \{ F(\alpha)\text{-embeddings } \varphi : K \to \overline{F} \} \leq [K : F(\alpha)]. $$ Therefore, by Theorem 1207, $$ \#\{ F\text{-embeddings } \varphi : K \to \overline{F} \} \leq [F(\alpha) : F][K : F(\alpha)] = [K : F]. $$ The equality holds if and only if the equality holds for $$ \#\{ F\text{-embeddings }\varphi : F(\alpha) \to \overline{F} \} = \# \{ \text{roots of }m_{\alpha, F}(x) \text{ in }\overline{F} \} \leq [F(\alpha) : F]. $$ So only if $$ \begin{align*} &\# \{ \text{roots of }m_{\alpha, F}(x) \text{ in } \overline{F} \} = [F(\alpha) : F] = \deg m_{\alpha, F}(x) \\ \iff &\text{all roots of }m_{\alpha, F}(x)\text{ are simple} \\ \iff &\alpha\text{ is separable over }F. \end{align*} $$ Since $\alpha \in K - F$ is arbitrarily chosen, it implies that the equality holds if and only if all $\alpha \in K - F$ is separable over $F$, so if and only if $K / F$ is separable.