[proofplan] We prove the equivalence between normality of $F/k$ and normality of $H$ in $G$ by analysing the restriction map $\operatorname{Gal}(K/k) \to \operatorname{Aut}_k(F)$. For the forward direction, normality of $F/k$ ensures every $\sigma \in G$ maps $F$ to itself (by the [Normality and Conjugate Embeddings](/theorems/3314) criterion), so conjugation by $\sigma$ preserves $H$. For the converse, $H \trianglelefteq G$ implies $\sigma(F) = F$ for every $\sigma \in G$, which yields normality of $F/k$ by the same criterion. The isomorphism $\operatorname{Gal}(F/k) \cong G/H$ then follows from the surjectivity of the restriction map with kernel $H$. [/proofplan] [step:Establish the restriction map from $G$ to automorphisms of $F$] Define the restriction map \begin{align*} \rho: G &\to \operatorname{Aut}_k(\overline{k}) \\ \sigma &\mapsto \sigma|_F \end{align*} where we view $\sigma|_F$ as a $k$-embedding $F \to \overline{k}$ (the restriction of $\sigma$ to $F$ is a $k$-homomorphism and hence injective). Note that $\sigma|_F$ is always a well-defined $k$-embedding of $F$ into $\overline{k}$, but it is not a priori an automorphism of $F$; the image $\sigma(F)$ may not equal $F$. The kernel of $\rho$ (once we establish its range) will play a central role. Observe that $\sigma|_F = \operatorname{id}_F$ if and only if $\sigma$ fixes every element of $F$, which is exactly the condition $\sigma \in \operatorname{Gal}(K/F) = H$. Thus $\ker \rho = H$ in the appropriate sense: $\sigma$ and $\tau$ have the same restriction to $F$ if and only if $\sigma^{-1}\tau \in H$. [/step] [step:Show that normality of $F/k$ implies $H \trianglelefteq G$] Assume $F/k$ is a normal extension. Since $K/k$ is Galois (hence separable), $F/k$ is also separable (as a subextension of a separable extension). By the [Normality and Conjugate Embeddings](/theorems/3314) criterion applied to the finite separable extension $F/k$, every $k$-embedding $\sigma: F \to \overline{k}$ satisfies $\sigma(F) = F$. For any $\sigma \in G = \operatorname{Gal}(K/k)$, the restriction $\sigma|_F: F \to \overline{k}$ is a $k$-embedding. By the normality criterion, $\sigma(F) = F$. Therefore $\sigma|_F \in \operatorname{Aut}_k(F)$ for every $\sigma \in G$. Now we show $H \trianglelefteq G$. Let $\sigma \in G$ and $h \in H = \operatorname{Gal}(K/F)$. We must show $\sigma h \sigma^{-1} \in H$, i.e., $\sigma h \sigma^{-1}$ fixes $F$ pointwise. Let $a \in F$. Since $\sigma(F) = F$, there exists $b \in F$ with $\sigma(b) = a$, equivalently $b = \sigma^{-1}(a)$. Then: \begin{align*} (\sigma h \sigma^{-1})(a) = \sigma(h(\sigma^{-1}(a))) = \sigma(h(b)) = \sigma(b) = a, \end{align*} where $h(b) = b$ because $b \in F$ and $h \in \operatorname{Gal}(K/F)$ fixes $F$. Since this holds for all $a \in F$, we have $\sigma h \sigma^{-1} \in \operatorname{Gal}(K/F) = H$. Therefore $H \trianglelefteq G$. [guided] Assume $F/k$ is a normal extension. Since $K/k$ is Galois, it is in particular separable, so the subextension $F/k$ is also separable. Being both finite and separable, we can apply the [Normality and Conjugate Embeddings](/theorems/3314) criterion: $F/k$ is normal if and only if every $k$-embedding $F \to \overline{k}$ maps $F$ onto itself. For any $\sigma \in G$, the restriction $\sigma|_F$ is a $k$-embedding of $F$ into $\overline{k}$ (since $\sigma$ fixes $k$ and $F \supset k$). The normality of $F/k$ forces $\sigma(F) = F$. This is the key consequence: every Galois automorphism of $K$ preserves $F$ as a set. Why does $\sigma(F) = F$ for all $\sigma \in G$ imply $H \trianglelefteq G$? We check the definition directly: for $\sigma \in G$ and $h \in H$, we need $\sigma h \sigma^{-1} \in H$, meaning $\sigma h \sigma^{-1}$ fixes every element of $F$. Take any $a \in F$. Since $\sigma(F) = F$ and $\sigma$ is bijective, $\sigma^{-1}(a) \in F$ as well. Then $h$ fixes $\sigma^{-1}(a)$ (because $h \in H = \operatorname{Gal}(K/F)$), so: \begin{align*} (\sigma h \sigma^{-1})(a) = \sigma(h(\sigma^{-1}(a))) = \sigma(\sigma^{-1}(a)) = a. \end{align*} Since $a \in F$ was arbitrary, $\sigma h \sigma^{-1}$ fixes $F$ pointwise, hence lies in $H$. This confirms $\sigma H \sigma^{-1} \subset H$ for every $\sigma \in G$, so $H \trianglelefteq G$. [/guided] [/step] [step:Show that $H \trianglelefteq G$ implies $F/k$ is a normal extension] Conversely, assume $H \trianglelefteq G$. We show $F/k$ is normal by verifying that every $k$-embedding of $F$ into $\overline{k}$ maps $F$ onto itself, then invoking the [Normality and Conjugate Embeddings](/theorems/3314) criterion. Let $\tau: F \to \overline{k}$ be any $k$-embedding. By the [Extension of Embeddings to Algebraic Closures](/theorems/3322) (applied to the algebraic extension $K/F$ and the embedding $\tau: F \to \overline{k}$), $\tau$ extends to an embedding $\tilde{\tau}: K \to \overline{k}$. Since $K/k$ is Galois (hence normal and separable), the [Normality and Conjugate Embeddings](/theorems/3314) criterion applied to $K/k$ gives $\tilde{\tau}(K) = K$, so $\tilde{\tau} \in G = \operatorname{Gal}(K/k)$. We claim $\tilde{\tau}(F) = F$. Let $a \in F$. By the [Fundamental Theorem of Galois Theory](/theorems/1274), $F = K^H$, i.e., $F$ is exactly the set of elements fixed by every $h \in H$. For any $h \in H$, since $H \trianglelefteq G$ we have $\tilde{\tau}^{-1} h \tilde{\tau} \in H$. Therefore: \begin{align*} h(\tilde{\tau}(a)) = \tilde{\tau}((\tilde{\tau}^{-1} h \tilde{\tau})(a)) = \tilde{\tau}(a), \end{align*} where the last equality holds because $\tilde{\tau}^{-1} h \tilde{\tau} \in H$ fixes $a \in F = K^H$. Since $h(\tilde{\tau}(a)) = \tilde{\tau}(a)$ for every $h \in H$, we have $\tilde{\tau}(a) \in K^H = F$. This shows $\tilde{\tau}(F) \subset F$. Since $\tilde{\tau}|_F = \tau$ and $\tau: F \to F$ is an injective $k$-linear map between finite-dimensional $k$-vector spaces of the same dimension $[F : k]$, it is surjective. Hence $\tau(F) = F$. Since every $k$-embedding $F \to \overline{k}$ maps $F$ onto itself, the [Normality and Conjugate Embeddings](/theorems/3314) criterion gives that $F/k$ is normal. (Note: $F/k$ is separable since it is a subextension of the separable extension $K/k$, so the criterion applies.) [guided] Conversely, assume $H = \operatorname{Gal}(K/F) \trianglelefteq G$. We want to show $F/k$ is normal. The strategy is to show every $k$-embedding of $F$ into $\overline{k}$ preserves $F$, then invoke the [Normality and Conjugate Embeddings](/theorems/3314) criterion. Let $\tau: F \to \overline{k}$ be a $k$-embedding. Can we extend $\tau$ to all of $K$? Yes: by the [Extension of Embeddings to Algebraic Closures](/theorems/3322), the embedding $\tau: F \to \overline{k}$ extends to an embedding $\tilde{\tau}: K \to \overline{k}$ (since $K/F$ is algebraic). Now $K/k$ is Galois, hence normal, so the [Normality and Conjugate Embeddings](/theorems/3314) criterion applied to $K/k$ gives $\tilde{\tau}(K) = K$. This means $\tilde{\tau} \in \operatorname{Aut}_k(K) = G$. Now we show $\tilde{\tau}(F) = F$. The [Fundamental Theorem of Galois Theory](/theorems/1274) tells us $F = K^H$, i.e., $F$ consists of exactly those elements of $K$ fixed by every automorphism in $H$. Take any $a \in F$ and any $h \in H$. We compute: \begin{align*} h(\tilde{\tau}(a)) = \tilde{\tau}\bigl((\tilde{\tau}^{-1} h \tilde{\tau})(a)\bigr). \end{align*} Since $H \trianglelefteq G$, the conjugate $\tilde{\tau}^{-1} h \tilde{\tau}$ belongs to $H$. Since $a \in F = K^H$, this conjugate fixes $a$: $(\tilde{\tau}^{-1} h \tilde{\tau})(a) = a$. Therefore $h(\tilde{\tau}(a)) = \tilde{\tau}(a)$. This holds for every $h \in H$, so $\tilde{\tau}(a) \in K^H = F$. Since $a \in F$ was arbitrary, $\tilde{\tau}(F) \subset F$. Restricting, $\tau = \tilde{\tau}|_F: F \to F$ is injective (as a field homomorphism) and $k$-linear between spaces of dimension $[F : k]$, hence surjective. So $\tau(F) = F$. What if $H$ were not normal? Then for some $\sigma \in G$ and $h \in H$, the conjugate $\sigma^{-1} h \sigma$ would not lie in $H$, meaning it would not fix all of $F$. So there would exist $a \in F$ with $h(\sigma(a)) \neq \sigma(a)$ for some $h \in H$, i.e., $\sigma(a) \notin K^H = F$. This gives a $k$-embedding of $F$ that escapes $F$ -- exactly the failure of normality. [/guided] [/step] [step:Construct the isomorphism $\operatorname{Gal}(F/k) \cong G/H$ when $H \trianglelefteq G$] Assume $H \trianglelefteq G$. By the previous step, every $\sigma \in G$ satisfies $\sigma(F) = F$, so the restriction map \begin{align*} \rho: G &\to \operatorname{Aut}_k(F) \\ \sigma &\mapsto \sigma|_F \end{align*} has image in $\operatorname{Aut}_k(F)$. Moreover, each $\sigma|_F$ fixes $k$ pointwise, so $\operatorname{im}(\rho) \subset \operatorname{Gal}(F/k)$. **$\rho$ is a group homomorphism.** For $\sigma, \tau \in G$ and $a \in F$: $\rho(\sigma\tau)(a) = (\sigma\tau)(a) = \sigma(\tau(a)) = \rho(\sigma)(\rho(\tau)(a))$, so $\rho(\sigma\tau) = \rho(\sigma) \circ \rho(\tau)$. **Kernel.** $\ker \rho = \{\sigma \in G : \sigma|_F = \operatorname{id}_F\} = \operatorname{Gal}(K/F) = H$. **Surjectivity.** Let $\phi \in \operatorname{Gal}(F/k)$. By the [Extension of Embeddings to Algebraic Closures](/theorems/3322), $\phi$ extends to an embedding $\tilde{\phi}: K \to \overline{k}$. Since $K/k$ is normal, $\tilde{\phi}(K) = K$ by the [Normality and Conjugate Embeddings](/theorems/3314) criterion, so $\tilde{\phi} \in G$. Then $\rho(\tilde{\phi}) = \tilde{\phi}|_F = \phi$, proving surjectivity. By the first isomorphism theorem for groups, $\rho$ induces an isomorphism: \begin{align*} G / H = G / \ker \rho \xrightarrow{\;\sim\;} \operatorname{im}(\rho) = \operatorname{Gal}(F/k). \end{align*} [guided] Assume $H \trianglelefteq G$. We have shown that every $\sigma \in G$ maps $F$ to itself, so the restriction $\sigma|_F$ is an automorphism of $F$ fixing $k$. This defines a map $\rho: G \to \operatorname{Gal}(F/k)$ by $\sigma \mapsto \sigma|_F$. **$\rho$ is a homomorphism.** This follows from the fact that restriction commutes with composition: for $\sigma, \tau \in G$ and $a \in F$, \begin{align*} \rho(\sigma\tau)(a) = (\sigma\tau)(a) = \sigma(\tau(a)) = \rho(\sigma)(\rho(\tau)(a)). \end{align*} **Kernel of $\rho$.** An automorphism $\sigma \in G$ lies in $\ker \rho$ if and only if $\sigma|_F = \operatorname{id}_F$, i.e., $\sigma$ fixes every element of $F$. This is precisely the defining condition for $\sigma \in \operatorname{Gal}(K/F) = H$. So $\ker \rho = H$. **Surjectivity of $\rho$.** This is the non-trivial part. Let $\phi \in \operatorname{Gal}(F/k)$ be any automorphism of $F$ fixing $k$. Can we extend $\phi$ to an automorphism of $K$? By the [Extension of Embeddings to Algebraic Closures](/theorems/3322), the $k$-embedding $\phi: F \to \overline{k}$ extends to an embedding $\tilde{\phi}: K \to \overline{k}$ (since $K/F$ is algebraic). Because $K/k$ is Galois (hence normal), the [Normality and Conjugate Embeddings](/theorems/3314) criterion gives $\tilde{\phi}(K) = K$, so $\tilde{\phi} \in G$. Since $\tilde{\phi}|_F = \phi$, we have $\rho(\tilde{\phi}) = \phi$, confirming surjectivity. Now the first isomorphism theorem for groups gives: \begin{align*} G / H = G / \ker \rho \xrightarrow{\;\sim\;} \operatorname{Gal}(F/k). \end{align*} As a consistency check: $|G/H| = |G|/|H| = [K : k]/[K : F] = [F : k]$, which equals $|\operatorname{Gal}(F/k)|$ since $F/k$ is Galois (being normal and separable as a subextension of the Galois extension $K/k$). This confirms the isomorphism is between groups of the correct order. [/guided] [/step]