Constructing Galois extensions. In Wiki Page I found the following statement. 
A result of Emil Artin allows one to construct Galois extensions as follows: If $E$ is a given field, and $G$ is a finite group of automorphisms of $E$ with fixed field $F$, then $E$ over  $F$ is a Galois extension.
Somebody please explain me, why the above statement is true.
Any hint is welcome. Thanks in advance.
 A: First we show that $E/F$ is finite, of degree less than or equal to $m = |G|$.
Let $\alpha \in E$. Let $\alpha=\alpha_1,\dots\alpha_r$ be the orbit of $\alpha$ under $G$, $r \leq m$. Then define $f(X) = \Pi(X-\alpha_i)$. $f$ is separable by definition and is fixed by every element of $G$, since any element of $G$ simply permutes the roots. Since $F = E^G$, this means $f \in F[X]$, so in particular $\alpha$ is algebraic over $F$. Also, the minimal polynomial of $\alpha $ over $F$ divides $f$, so is separable. Thus we have shown that $E/F$ is both algebraic and separable, and that for all $\alpha \in E$, $[F(\alpha):F]\leq m$.
Now let $\alpha$ be an element such that $[F(\alpha):F]$ is maximal. If $F(\alpha) \not = E$, take $\beta \in E\backslash F(\alpha)$. $E/F$ is separable, so by the primitive element theorem, $F(\alpha,\beta)= F(\gamma)$ for some $\gamma \in E$, with $[F(\gamma):F]>[F(\alpha):F]$. Contradiction.
Now all that remains to be shown is that $G = Aut(E/F)$. Certainly $G \subset Aut(E/F)$. But $E/F$ is finite, so $|Aut(E/F)|\leq[E:F]\leq|G|\leq|Aut(E/F)|$. Thus we have equivalence at each point in the equality, so in particular $G = Aut(E/F)$.
This is a great theorem, because it allows us to prove things like the fact that for in integral domain $R$, $R[X_1,\dots,X_n]/Sym_n$ where $Sym_n$ is the symmetric polynomials over $R$ with $n$ variables is finite and Galois. This is both hard to do otherwise, quite interesting, and useful in e.g. finding polynomials which have insoluble Galois groups. It also allows us to show that the characterisation of Galois extensions as those where $|E/F| = |Aut(E/F)|$ is equivalent to the definitions "$E/F$ is normal and separable" or "$E^{Aut(E/F)} = F$".
