let G be strict solvable Group; :: thesis: for H being strict Subgroup of G holds H is solvable
let H be strict Subgroup of G; :: thesis: H is solvable
consider F being FinSequence of Subgroups G such that
A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) ) by Def1;
defpred S₁[ set , set ] means ex I being strict Subgroup of G st
( I = F . $1 & $2 = I /\ H );
A2: for k being Nat st k in Seg (len F) holds
ex x being Element of Subgroups H st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of Subgroups H st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of Subgroups H st S₁[k,x]
then k in dom F by FINSEQ_1:def 3;
then F . k in Subgroups G by FINSEQ_2:13;
then reconsider I = F . k as strict Subgroup of G by GROUP_3:def 1;
reconsider x = I /\ H as strict Subgroup of H by GROUP_2:106;
reconsider y = x as Element of Subgroups H by GROUP_3:def 1;
take y ; :: thesis: S₁[k,y]
take I ; :: thesis: ( I = F . k & y = I /\ H )
thus ( I = F . k & y = I /\ H ) ; :: thesis: verum

end;

consider R being FinSequence of Subgroups H such that
A3: ( dom R = Seg (len F) & ( for i being Nat st i in Seg (len F) holds
S₁[i,R . i] ) ) from FINSEQ_1:sch 5(A2);
A4: len R = len F by A3, FINSEQ_1:def 3;
A5: len R > 0 by A1, A3, FINSEQ_1:def 3;
A6: R . 1 = (Omega). H

proof

1 <= len R by A5, NAT_1:14;
then 1 in Seg (len F) by A4, FINSEQ_1:3;
then consider I being strict Subgroup of G such that
A7: ( I = F . 1 & R . 1 = I /\ H ) by A3;
thus R . 1 = (Omega). H by A1, A7, GROUP_2:104; :: thesis: verum

end;

A8: R . (len R) = (1). H

proof

len R in Seg (len F) by A1, A4, FINSEQ_1:5;
then consider I being strict Subgroup of G such that
A9: ( I = F . (len R) & R . (len R) = I /\ H ) by A3;
thus R . (len R) = (1). G by A1, A4, A9, GROUP_2:103
.= (1). H by GROUP_2:75 ; :: thesis: verum

end;

A10: for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being strict Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )

proof

let i be Element of NAT ; :: thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being strict Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A11: ( i in dom R & i + 1 in dom R ) ; :: thesis: for H1, H2 being strict Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
let H1, H2 be strict Subgroup of H; :: thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A12: ( H1 = R . i & H2 = R . (i + 1) ) ; :: thesis: ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
consider I being strict Subgroup of G such that
A13: ( I = F . i & R . i = I /\ H ) by A3, A11;
consider J being strict Subgroup of G such that
A14: ( J = F . (i + 1) & R . (i + 1) = J /\ H ) by A3, A11;
A15: ( i in dom F & i + 1 in dom F ) by A3, A11, FINSEQ_1:def 3;
then reconsider J1 = J as strict normal Subgroup of I by A1, A13, A14;
A16: ( H1 = I /\ H & H2 = J1 /\ H ) by A12, A13, A14;
for N being strict normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative

proof

let N be strict normal Subgroup of H1; :: thesis: ( N = H2 implies H1 ./. N is commutative )
assume N = H2 ; :: thesis: H1 ./. N is commutative
then consider G3 being Subgroup of I ./. J1 such that
A17: H1 ./. N,G3 are_isomorphic by A12, A13, A14, Th4;
consider h being Homomorphism of (H1 ./. N),G3 such that
A18: h is bijective by A17, GROUP_6:def 15;
A19: ( h is onto & h is one-to-one ) by A18, FUNCT_2:def 4;
I ./. J1 is commutative by A1, A13, A14, A15;
then A20: G3 is commutative ;
H1 ./. N is commutative

proof

now

let a, b be Element of (H1 ./. N); :: thesis: the multF of (H1 ./. N) . a,b = the multF of (H1 ./. N) . b,a
consider a' being Element of G3 such that
A21: a' = h . a ;
consider b' being Element of G3 such that
A22: b' = h . b ;
the multF of G3 is commutative by A20, GROUP_3:2;
then A23: a' * b' = b' * a' by BINOP_1:def 2;
thus the multF of (H1 ./. N) . a,b = (h " ) . (h . (a * b)) by A19, FUNCT_2:32
.= (h " ) . ((h . b) * (h . a)) by A21, A22, A23, GROUP_6:def 7
.= (h " ) . (h . (b * a)) by GROUP_6:def 7
.= the multF of (H1 ./. N) . b,a by A19, FUNCT_2:32 ; :: thesis: verum

end;

then the multF of (H1 ./. N) is commutative by BINOP_1:def 2;
hence H1 ./. N is commutative by GROUP_3:2; :: thesis: verum

end;

hence H1 ./. N is commutative ; :: thesis: verum

end;

hence ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) by A16, Th1; :: thesis: verum

end;

take R ; :: according to GRSOLV_1:def 1 :: thesis: ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for G1, G2 being strict Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) )
thus ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for G1, G2 being strict Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) ) by A1, A3, A6, A8, A10, FINSEQ_1:def 3; :: thesis: verum