A simpler proof of an important statement in the book "Galois Theory" by Ian Stewart Reading the book "Galois Theory" (3rd ed.) by Ian Stewart, I try for better understanding and possible
future formalization to rewrite  Stewart's proof of a very important Lemma 15.7
If $K$ is a subfield of $\mathbb{C}$ and $L:K$
is normal and radical then $\Gamma(L:K)$ is soluble 
in a more structured way (see "Structuring Mathematical Proofs" by Uri Leron and 
"How to Write a 21st Century Proof" by Leslie Lamport, available for free via Google, as well as the book).
Let us remind some definitions (all fields here are subfields of $\mathbb{C}$).
Definition 1. A simple radical extension is a field extension $L:K$, if there exist $n,a$ such that $n \in \mathbb{N}, a \in \mathbb{C}, a \notin K,
a^n \in K, L = K(a)$.
Definition 2. A prime simple radical extension is a simple radical extension $L:K$, if  $n$ in Definition 1 is a prime number. 
Lemma 1. If $K(a):K$ is a normal prime simple radical extension, where $a^p \in K$then $L$ contains all $pth$ roots of unity.
  A proof of Lemma 1 can be extracted from Stewart's proof of Lemma 15.7 (the lines 7-12 of the proof).
Lemma 2. If $L:K$ is a normal prime simple radical extension, then $\Gamma(L:K)$ is abelian.   Follows from Lemma 15.5 in the book and Lemma 1.
Lemma 3. For any radical extension $L:K$, there exists a sequence of subfields
$K = M_{0} \subset M_{1} \subset M_{2} \ldots \subset M_{n} = L$  where $n \geq 0$  
such that $M_i : M_{i-1}$ is a prime simple radical extension $(i=1,2,\ldots,n)$.
It is Proposition 8.9 in the book.
Now a simpler proof of Lemma 15.7 can be written as follows:
By Lemma 3, there exists a sequence of subfields
$K = M_{0} \subset M_{1} \subset M_{2} \ldots \subset M_{n} = L$  where $n \geq 0$ 
such that $M_{i} : M_{i-1}$ is a prime simple radical extension, $i=1,2, \ldots, n$ . 
Now proceed by induction on $n$. 
If $n=0$ then $L=K$ and $\Gamma(K:K)$ is a trivial group which is abelian and therefore solvable.
If $n>0$ then $K \subset N  \subset L$, where $N = M_{n-1}$.
The extension $L:N$ is normal (because $L:K$ is normal and $N$ is an intermediate field).
By Theorem 12.4(4), $\Gamma(L:N)$ is normal in $\Gamma(L:K)$.
By Theorem 12.4(5), $\Gamma(N:K) \cong \Gamma(L:K) / \Gamma(L:N)$.
By induction, $\Gamma(N:K)$ is soluble.
By Lemma 2, $\Gamma(L:N)$ is abelian and therefore soluble.
Therefore, by Theorem 14.4(3) $\Gamma(L:K)$ is soluble.
End of proof of Lemma 15.7.
Is this proof correct?
Any comments are welcome.
 A: Both the proof in the book and your proof seem to me pretty messy, involved and long, but this could be due to the fact that neither you nor Stewart assume some slightly deeper knowledge of what soluble groups are but the very definition, and also because some facts about automorphism of fields extensions are lacking (I can't tell: I haven't read the book). 
I'd go as follows, using your notation:
By lemma $\;3\;$ there exists a sequence of fields $\;K=:M_0\subset M_1\subset\ldots\subset M_n:=L\;$ , s.t. $\; M_i:M_{i-1}\;$ is a a prime simple radical extension.
But by lemma $\;2\;$ it then follows that $\;\Gamma (M_i:M_{i-1})\;$ is abelian. Thus, there exists in $\;\Gamma (L:K)\;$ a subnormal series of abelian groups, which is exactly the definition of soluble group. $\;{}{}$ Q.E.D.
More surprising to me is that the above is the definition of soluble group in Stewart's book (because there is another usual, equivalent one by means of the derived series and stuff), so I'm not sure why the proof comes up so long and messy, though I can understand the use of induction but only to make sure the argument about the abelian series is completely formal.
