Splitting field of a separable polynomial is separable Probably a stupid question, but..
Why is the splitting field of a separable polynomial necessarily separable?
Thanks.
Follow up question
Show that if $F$ is a splitting field over $K$ for $P \in K[X]$, then $[F:K] \leq n!$
I've proven this by induction on $n$, but I'm convinced there's a more algebraic approach ($n!$ screams $S_n$). 
If I knew $P$ were separable, then I'd know $F$ was Galois, so $ |\mbox{Gal}(F/K)| = [F:K] $. Considering the action of $ \mbox{Gal}(F/K) $ on the roots of $P$, we'd get an injective homomorphism into $ S_n $, giving the result. 
But $P$ is not given to be separable, so $P$ could have repeated roots when factorised in $F$. If $G$ is any finite group of $K$-automorphisms of $L$, then I know that $[F:K] \leq |G| $. Considering the action of $G$ on the set of roots of $P$, say $\Omega$, we get an injective homomorphism of $G$ into $S_{|\Omega|}$, where $|\Omega| \leq n$ (I think). I have a feeling I'm wrong here, since I think $G$ is forced to be $\mbox{Aut}(F/K)$. Any advice would be appreciated.
 A: New Answer
[New version of the new answer. Thank you very much to KCd! --- See his comment.]
The simplest, I think, is to prove the Fundamental Theorem of Galois Theory (FTGT) for a normal extension $E/F$ generated by finitely many separable elements, and to obtain the fact that all the elements of $E$ are separable over $F$ as a corollary. 
The point is that the FTGT can be given a very short proof, which will be described below. (I of course believe that this proof is complete. Thanks for correcting me if I'm wrong.)

FTGT (Fundamental Theorem of Galois Theory). Let $F$ be a field, let $A$ be an algebraic closure of $F$, let $p\in F[X]$ be a product of separable irreducible polynomials, let $E$ be a splitting field for $p$ over $F$, and let $a_1,\dots,a_n$ be the roots of $p$ in $E$. Then
  
  
*
  
*the group $G$ of $F$-automorphisms of $E/F$ is finite,
  
*there is a bijective correspondence between the sub-extensions $S/F$ of $E/F$ and the subgroups $H$ of $G$, and we have
  $$
S\leftrightarrow H\iff H=\text{Aut}_S E\iff S=E^H\implies[E:S]=|H|,
$$
  where $E^H$ is the fixed subfield of $H$, where $[E:S]$ is the degree (that is the dimension) of $E$ over $S$, and where $|H|$ is the order of $H$.

We are taking for granted 
$(1)$ the universal property of a simple algebraic extension, and 
$(2)$ the existence and universal property of our splitting field $E$,
which we briefly recall: 
$(1)$ If $a$ is algebraic over a field $K$, then the $K$-embeddings of $K(a)$ in an extension $L$ of $K$ are in natural bijection with the roots in $L$ of the minimal polynomial of $a$ over $K$.
$(2)$ Any root of $p$ in any extension of $E$ is in $E$, and $E$ is generated over $F$ by the roots $a_i$ of $p$. Moreover, if $S/F$ is a sub-extension of $E/F$, then any $F$-embedding of $S$ in $E$ extends to an $F$-automorphism of $E$.
Going back to the assumptions of the FTGT, we claim:  
$(3)$ If $S/F$ is a sub-extension of $E/F$, then $[E:S]=|\text{Aut}_S E|$.  
$(4)$ If $H$ is a subgroup of $G$, then $|H|=[E:E^H]$.  
Proof that (3) and (4) imply the FTGT. Let $S/F$ be a sub-extension of $E/F$ and put $H:=\text{Aut}_S E$. Then we have trivially $S\subset E^H$, and $(3)$ and $(4)$ imply 
$$
[E:S]=[E:E^H].
$$
Conversely let $H$ be a subgroup of $G$ and set $\overline H:=\text{Aut}_{E^H}E$. Then we have trivially $H\subset\overline H$, and $(3)$ and $(4)$ imply $|H|=|\overline H|$.
To prove that any element $a$ of $E$ is separable over $F$, put $H:=\text{Aut}_{F(a)}E$, and note that the set of $F$-embeddings of $F(a)$ in $E$ is in natural bijection with the set $G/H$, whose cardinality is, by the FTGT, equal to $[F(a):F]$.
Proof of (3). The statement follows from the fact that any $F$-embedding of $S_i:=S(a_1,\dots,a_i)$ in $E$ has exactly $[S_{i+1}:S_i]$ extensions to $S_{i+1}$.
Proof of (4). In view of (3) it is enough to check $|H|\ge[E:E^H]$. Let $k$ be an integer larger than $|H|$, and pick a 
$$
b=(b_1,\dots,b_k)\in E^k.
$$
We must show that the $b_i$ are linearly dependent over $E^H$, or equivalently that $b^\perp\cap(E^H)^k$ is nonzero, where $?^\perp$ denotes the vectors orthogonal to ? in $E^k$ with respect to the dot product on $E^k$. Any element of $b^\perp \cap (E^H)^k$ is necessarily orthogonal to $h(b)$ for any $h \in H$, so  $b^\perp \cap (E^H)^k = (Hb)^\perp \cap (E^H)^k$, where $Hb$ is the $H$-orbit of $H$. We will show $(Hb)^\perp \cap (E^H)^k$ is nonzero. Since the span of $Hb$ in $E^k$ has $E$-dimension at most $|H| < k$, $(Hb)^\perp$ is nonzero. Choose a nonzero vector $x$ in $(Hb)^\perp$ such that $x_i=0$ for the largest number of $i$ as possible among all nonzero vectors in $(Hb)^\perp$. Some coordinate $x_j$ is nonzero in $E$, so by scaling we can assume $x_j = 1$ for some $j$. Since the subspace $(Hb)^\perp$ in $E^k$ is stable under the action of $H$, for any $h$ in $H$ we have $h(x) \in (Hb)^\perp$, so $h(x)-x \in (Hb)^\perp$. Since $x_j = 1$, the $j$-th coordinate of $h(x) - x$ is $0$, so $h(x)-x = 0$ by the choice of $x$. Since this holds for all $h$ in $H$, $x$ is in $(E^H)^k$. 
Old Answer
This is more a hint than an answer. I think the key point here is to understand the equivalence between various definitions of a separable extension. I'll just try to emphasize some of the basic facts. 
Let $K$ be a field, $A/K$ an algebraic closure, and $L/K$ an extension of degree $d < \infty$ contained in $A$. We claim that the following conditions are equivalent:
(1) $L/K$ is generated by separable elements,
(2) each element of $L$ is separable over $K$,
(3) there are exactly $d$ embeddings of $L$ in $A$ over $K$.
We say that $L/K$ is separable if it satisfies these conditions. Let's sketch a proof of the equivalence.
Say that the number, denoted by $[L:K]_s$, of $K$-embeddings of $L$ in $A$ is the separable degree of $L/K$. 
Let $M$ be a finite degree extension of $K$ contained in $A$, and $L$ a field between $K$ and $M$. We claim:
(4) $[M:K]_s=[M:L]_s\ [L:K]_s$.
This is an easy, but instructive, exercise.
Claim: (1) and (3) are equivalent when $K$ is generated by a single element $\alpha$. Indeed, if $f\in K[X]$ is the minimal polynomial of $\alpha$, then $[L:K]$ is the degree of $f$, whereas $[L:K]_s$ is the number of distinct roots of $f$ in $A$.
In view of (4), the above claim implies that (1), (2) and (3) are equivalent in the general case.
As a corollary, we see that a finite degree extension $L/K$ contains a largest separable sub-extension $S$, and that $[S:K]=[L:K]_s$. 
As a corollary to the corollary, we get the fact suggested by the notation that the integer $[L:K]_s$ does not depend on the choice of an algebraic closure of $L$.
A: $\DeclareMathOperator{\aut}{Aut}$ $\newcommand{\vp}{\varphi}$Here is a short proof.
Let $E$ be the splitting field of a separable polynomial $p(x)$ over a field $F$. We need to show that $E:F$ is a separable extension.
Claim 1. $[E:F]=|\aut(E:F)|$.
Proof. Say $\deg p=n$ and let $a_1, \ldots, a_n$ be all the roots of $p$ in $E$. Write $F_i$ to denote $F(a_1, \ldots, a_i)$. We will show that each $F$-embedding of $F_i$ in $E$ admits exactly $[F_{i+1}:F_i]$ extensions to an embedding of $F_{i+1}$ into $E$.
Suppose $\vp:F_i\to E$ be an $F$-embedding of $F_i$ in $E$ and let $d_i=[F_{i+1}:F_i]$. We need to show that there are exactly $d_i$ different extensions of $\vp$ to an embedding of $F_{i+1}$ into $E$. Let $p_i(x)\in F_i[x]$ be the minimal polynomial of $a_i$ over $F_i$. Since $p_i$ and $p$ both have $a_{i+1}$ has a root, we have $p_i|p$ and therefore $p_i$ has $d_i$ distinct roots in $E$. Now we may extend $\vp$ to $F_{i+1}$ by sending $a_{i+1}$ to any root of $p_i$ we wish. Further, all extensions of $\vp$ send $a_{i+1}$ to some root of $p_i$. Lastly, any extension of $\vp$ is determined completely by its action on $a_{i+1}$. Therefore there are precisely $d_i=[F_{i+1}:F_i]$ different extensions of $\vp$ to $F_{i+1}$.
Thus there are at least $[F_n:F_{n-1}]\cdots [F_1:F]=[E:F]$ distinct elements in $\aut(E:F)$. There cannot be any more and thus we are done. $\blacksquare$
Claim 2. The fixed field in $E$ of $\aut(E:F)$ is $F$.
Proof. Let $M$ be the fixed field of $\aut(E:F)$. Thus there is a natural bijection between $\aut(E:M)$ and $\aut(E:F)$. Note that $p(x)$ is a separable polynomial over $M$ whose splitting field is $E$. Therefore, by Claim 1, we have $|\aut(E:M)|=[E:M]$. This shows that $|\aut(E:F)|=[E:M]$. In the light of Claim 1, this is only possible if $M=F$. $\blacksquare$
Claim 3. $E$ is separable over $F$.
Proof. Let $\alpha\in E$ be chosen arbitrarily and $f(x)$ be the minimal polynomial of $\alpha$ over $F$. We need to show that $f(x)$ is separable over $F$. Note that $E$ is normal over $F$ and therefore completely splits $f$. Write $f=(x-\beta_1)^{r_1}\cdots (x-\beta_k)^{r_k}$ in $E[x]$, where $\beta_i$'s are pairwise distinct. If $\vp\in \aut(E:F)$, then we see that
$$f=(x-\beta_1)^{r_1}\cdots (x-\beta_k)^{r_k}= (x-\vp(\beta_1))^{r_1}\cdots (x-\vp(\beta_k))^{r_k}$$
which lets us conclude that $\vp$ permutes $\{\beta_1, \ldots, \beta _k\}$. Since $\vp$ was arbitrary in $\aut(E:F)$, we conclude that $\aut(E:F)$ acts on $\{\beta_1, \ldots, \beta_k\}$. Therefore the symmetric functions on $\beta_i$'s remain fixed by $\aut(E:F)$. Applying Claim 2, we see that each symmetric function in $\beta_i$'s is a member of $F$. Therefore the polynomial $(x-\beta_1)\cdots (x-\beta_k)$ is in $F[x]$. Since $f(x)$ was irreducible over $F$, we are forced to have $f(x)=(x-\beta_1)\cdots (x-\beta_k)$ and we have shown that $\alpha$ is separable over $F$. $\blacksquare$
A: Here's another proof that the splitting field for a separable polynomial is separable.
First use the fact, proven by caffeinemachine above, that if $E$ is a splitting field by a separable polynomial over $F$ then $|\text{Aut}(E/F)| = |E:F|$. A simple note from the proof is that if the splitting polynomial isn't separable, then the group of automorphisms has strictly smaller cardinality, since there are strictly fewer extensions when there are duplicate roots.
Then, use the following lemma:
Lemma 1. If $K$ is characteristic in $E$ fixing $F$ (if $K$ is stable under every automorphism of $E/F$), with $F \subseteq K \subseteq E$, then $|\text{Aut}(E/K)||\text{Aut}(K/F)| \geq |\text{Aut}(E/F)|$.
Proof. Consider the equivalence relation on $\text{Aut}(E/F)$ where $\sigma \sim \tau$ if $\sigma \circ \tau^{-1}$ fixes $K$. This relation is symmetric, reflexive, and transitive. It is easy to see that the size of each coset is $\text{Aut}(E/K)$, since automorphisms are invertible. Two automorphisms are in the same coset if and only if they restrict to the same automorphism on $K$ that fixes $F$, since $\sigma \circ \tau^{-1}$ fixes $K$. This restriction is possible since $K$ is characteristic. So, the number of cosets is smaller than the number of automorphisms on $K$ that fix $F$. This proves that $\frac{|\text{Aut}(E/F)|}{|\text{Aut}(E/K)|} \leq |\text{Aut}(K/F)|$.
Now, take an element $\alpha$ of $E$, with minimal polynomial $g(x)$. Assume by contradiction that it is not separable. Then we know that $\text{Aut}(K/F) < |K:F| $, where K is the splitting field of $g(x)$ over $F$. Note that $K \subseteq E$, since $\alpha \in E$ and any irreducible polynomial with a root in a splitting field splits. So, we find that $|\text{Aut}(E/K)||\text{Aut}(K/F)| < |E:K||K:F| = |E:F|$. To complete the proof, observe that $K$ is characteristic in $E/F$, since the generators (the roots of the splitting polynomial) must permute with each other. So, $|\text{Aut}(E/K)||\text{Aut}(K/F)| \geq |\text{Aut}(E/F)| = |E:F|$, a contradiction.
