An algebraic extension that is a splitting field of a polynomial is normal

Fix $\alpha \in E$ and let $m$ be its minimal polynomial over $F$. By [F5], choose a splitting field $\mathrm{\Omega }\mathrm{/}E$ of $m$, and let $\beta$ be any root of $m$ in $\mathrm{\Omega }$. By [F1], the identity on $F$ extends to an isomorphism ${\sigma }_0:F(\alpha )\to F(\beta )$ sending $\alpha$ to $\beta$.

The field $E$ is a splitting field of $f$ over $F(\alpha )$, because it splits $f$ and is generated by its roots. The field $E(\beta )$ is a splitting field of $f$ over $F(\beta )$ for the same reason. Since ${\sigma }_0$ fixes the coefficients of $f$, [F2] extends it to an isomorphism $\sigma :E\to E(\beta )$.

Every generator of $E$ over $F$ is a root of $f$. The map $\sigma$ fixes $F$ and therefore carries each such generator to another root of $f$, all of which already lie in $E$. Hence $\sigma (E)\subseteq E$. But $\sigma (E)=E(\beta )$ by surjectivity, so $\beta \in E$.

Every root $\beta$ of the minimal polynomial $m$ lies in $E$, so $m$ splits over $E$. Since $\alpha$ was arbitrary and $E\mathrm{/}F$ is algebraic by hypothesis, [F4] proves normality.