[proofplan]
We prove both directions by exploiting the characterisation of normal extensions as splitting fields. For the forward direction, normality means $K$ is the splitting field of some separable polynomial $f \in k[x]$; since any $k$-embedding permutes the roots of $f$ and $K$ is generated by these roots, the image must equal $K$. For the converse, we take the minimal polynomials of a set of generators of $K/k$, show that the hypothesis forces every root of each minimal polynomial to lie in $K$, and conclude that $K$ is a splitting field.
[/proofplan]
[step:Show that normality forces every $k$-embedding to map $K$ onto itself]
Since $K/k$ is finite and separable, and $K/k$ is normal, by the [Normal Extensions Are Splitting Fields](/theorems/1269) characterisation, $K$ is the splitting field of some polynomial $f \in k[x]$ over $k$. Because $K/k$ is separable, $f$ is separable (its irreducible factors over $k$ are separable). Write $\alpha_1, \ldots, \alpha_m$ for the roots of $f$ in $K$, so that $K = k(\alpha_1, \ldots, \alpha_m)$.
Let $\sigma: K \to \overline{k}$ be a $k$-embedding. Since $\sigma$ fixes $k$ pointwise, for each root $\alpha_i$ of $f$ we have $f(\sigma(\alpha_i)) = \sigma(f(\alpha_i)) = \sigma(0) = 0$. Thus $\sigma(\alpha_i)$ is again a root of $f$. Since all roots of $f$ lie in $K$ (as $K$ is the splitting field of $f$), we have $\sigma(\alpha_i) \in K$ for every $i$. Because $\sigma$ is a $k$-algebra homomorphism and $K = k(\alpha_1, \ldots, \alpha_m)$, every element of $K$ is a $k$-polynomial expression in the $\alpha_i$, so $\sigma(K) \subset K$.
To show $\sigma(K) = K$, note that $\sigma: K \to K$ is an injective $k$-algebra homomorphism (field homomorphisms are injective). Since $K$ is a finite-dimensional $k$-vector space, an injective $k$-linear map $K \to K$ is surjective by dimension counting: $\dim_k \sigma(K) = \dim_k K = [K : k]$. Therefore $\sigma(K) = K$.
[guided]
**Forward direction.** Assume $K/k$ is normal. We want to show that every $k$-embedding $\sigma: K \to \overline{k}$ satisfies $\sigma(K) = K$.
Since $K/k$ is finite, separable, and normal, the [Normal Extensions Are Splitting Fields](/theorems/1269) characterisation tells us that $K$ is the splitting field of some polynomial $f \in k[x]$ over $k$. Write $\alpha_1, \ldots, \alpha_m$ for all the roots of $f$ in $\overline{k}$. Since $K$ is the splitting field of $f$, all these roots lie in $K$, and $K = k(\alpha_1, \ldots, \alpha_m)$.
Now let $\sigma: K \to \overline{k}$ be any $k$-embedding. What happens to the roots $\alpha_i$ under $\sigma$? Since $\sigma$ fixes $k$ pointwise, for each $i$:
\begin{align*}
f(\sigma(\alpha_i)) = \sigma(f(\alpha_i)) = \sigma(0) = 0.
\end{align*}
So $\sigma(\alpha_i)$ is again a root of $f$. But all roots of $f$ lie in $K$, so $\sigma(\alpha_i) \in K$ for every $i$. Since $K = k(\alpha_1, \ldots, \alpha_m)$ and $\sigma$ is a $k$-algebra homomorphism, every element of $K$ is a polynomial expression in the $\alpha_i$ with $k$-coefficients, and $\sigma$ maps it to the same polynomial expression applied to $\sigma(\alpha_1), \ldots, \sigma(\alpha_m) \in K$. Therefore $\sigma(K) \subset K$.
Why is $\sigma$ surjective? Because $\sigma: K \to K$ is an injective $k$-linear map (all field homomorphisms are injective) between finite-dimensional $k$-vector spaces of the same dimension $[K : k]$. By the rank-nullity theorem for linear maps, injectivity forces surjectivity. Hence $\sigma(K) = K$, and $\sigma$ restricts to an automorphism of $K$ fixing $k$.
[/guided]
[/step]
[step:Show that the embedding condition implies normality]
Conversely, assume every $k$-embedding $\sigma: K \to \overline{k}$ satisfies $\sigma(K) = K$. We show $K/k$ is normal by verifying that $K$ is a splitting field over $k$.
Since $K/k$ is finite and separable, the [Primitive Element Theorem](/theorems/1267) gives $K = k(\alpha)$ for some $\alpha \in K$. Let $f = \operatorname{min}(\alpha, k) \in k[x]$ be the minimal polynomial of $\alpha$ over $k$, with $\deg f = [K : k] = n$. In the algebraic closure $\overline{k}$, write the roots of $f$ as $\alpha_1 = \alpha, \alpha_2, \ldots, \alpha_n$.
For each root $\alpha_j$, there is a $k$-embedding $\sigma_j: K \to \overline{k}$ defined by $\sigma_j(\alpha) = \alpha_j$. This is well-defined because $f$ is the minimal polynomial of $\alpha$ over $k$, and any assignment $\alpha \mapsto \alpha_j$ (where $\alpha_j$ is a root of $f$) extends to a $k$-homomorphism $k(\alpha) \to \overline{k}$.
By hypothesis, $\sigma_j(K) = K$ for each $j$. In particular, $\alpha_j = \sigma_j(\alpha) \in \sigma_j(K) = K$. Since every root of $f$ lies in $K$, the polynomial $f$ splits completely over $K$:
\begin{align*}
f(x) = \prod_{j=1}^{n} (x - \alpha_j) \in K[x].
\end{align*}
Since $K = k(\alpha) = k(\alpha_1)$ and $\alpha_1, \ldots, \alpha_n \in K$, we have $K = k(\alpha_1, \ldots, \alpha_n)$, which is the splitting field of $f$ over $k$. By the [Normal Extensions Are Splitting Fields](/theorems/1269) characterisation, $K/k$ is normal.
[guided]
**Converse direction.** Assume every $k$-embedding $\sigma: K \to \overline{k}$ satisfies $\sigma(K) = K$. We need to show $K/k$ is normal, i.e., that $K$ is the splitting field of some polynomial over $k$.
The strategy is: take a generator of $K/k$ and show its minimal polynomial splits completely in $K$. Since $K/k$ is finite and separable, the [Primitive Element Theorem](/theorems/1267) guarantees a primitive element: there exists $\alpha \in K$ with $K = k(\alpha)$. Let $f = \operatorname{min}(\alpha, k) \in k[x]$ be its minimal polynomial, which has degree $n = [K : k]$. Write $\alpha_1 = \alpha, \alpha_2, \ldots, \alpha_n$ for the roots of $f$ in $\overline{k}$ (these are all distinct since $K/k$ is separable, so $f$ is separable).
For each root $\alpha_j$, can we build a $k$-embedding sending $\alpha$ to $\alpha_j$? Yes: since $f(\alpha_j) = 0$ and $f$ is the minimal polynomial of $\alpha$, there is a unique $k$-isomorphism $k(\alpha) \to k(\alpha_j)$ sending $\alpha \mapsto \alpha_j$. Composing with the inclusion $k(\alpha_j) \hookrightarrow \overline{k}$ gives a $k$-embedding $\sigma_j: K = k(\alpha) \to \overline{k}$ with $\sigma_j(\alpha) = \alpha_j$.
Now we apply our hypothesis: $\sigma_j(K) = K$. In particular, $\alpha_j = \sigma_j(\alpha) \in K$. This holds for every $j = 1, \ldots, n$. So all $n$ roots of $f$ lie in $K$, meaning $f$ splits completely over $K$:
\begin{align*}
f(x) = \prod_{j=1}^{n} (x - \alpha_j) \in K[x].
\end{align*}
Moreover, $K = k(\alpha) \subset k(\alpha_1, \ldots, \alpha_n) \subset K$ (since each $\alpha_j \in K$), so $K = k(\alpha_1, \ldots, \alpha_n)$ is the splitting field of $f$ over $k$. By the [Normal Extensions Are Splitting Fields](/theorems/1269) characterisation, $K/k$ is normal.
What would fail without the hypothesis? If some $k$-embedding $\sigma_j$ had $\sigma_j(K) \neq K$, then $\alpha_j = \sigma_j(\alpha)$ might not lie in $K$, and $f$ would not split over $K$ -- exactly the failure of normality.
[/guided]
[/step]