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 and
A2: F . 1 = (Omega). G and
A3: F . (len F) = (1). G and
A4: 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 );
A5: 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:11;
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:88;
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
A6: ( 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(A5);
A7: 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 that
A8: i in dom R and
A9: 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 ) )
consider J being strict Subgroup of G such that
A10: J = F . (i + 1) and
A11: R . (i + 1) = J /\ H by A6, A9;
consider I being strict Subgroup of G such that
A12: I = F . i and
A13: R . i = I /\ H by A6, A8;
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 that
A14: H1 = R . i and
A15: 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 ) )
A16: ( i in dom F & i + 1 in dom F ) by A6, A8, A9, FINSEQ_1:def 3;
then reconsider J1 = J as strict normal Subgroup of I by A4, A12, A10;
A17: 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
A18: H1 ./. N,G3 are_isomorphic by A14, A15, A13, A11, Th4;
consider h being Homomorphism of (H1 ./. N),G3 such that
A19: h is bijective by A18, GROUP_6:def 11;
A20: h is one-to-one by A19, FUNCT_2:def 4;
A21: I ./. J1 is commutative by A4, A12, A10, A16;

now :: thesis: for a, b being Element of (H1 ./. N) holds the multF of (H1 ./. N) . (a,b) = the multF of (H1 ./. N) . (b,a)

let a, b be Element of (H1 ./. N); :: thesis: the multF of (H1 ./. N) . (a,b) = the multF of (H1 ./. N) . (b,a)
consider a9 being Element of G3 such that
A22: a9 = h . a ;
consider b9 being Element of G3 such that
A23: b9 = h . b ;
the multF of G3 is commutative by A21, GROUP_3:2;
then A24: a9 * b9 = b9 * a9 by BINOP_1:def 2;
thus the multF of (H1 ./. N) . (a,b) = (h ") . (h . (a * b)) by A20, FUNCT_2:26
.= (h ") . ((h . b) * (h . a)) by A22, A23, A24, GROUP_6:def 6
.= (h ") . (h . (b * a)) by GROUP_6:def 6
.= the multF of (H1 ./. N) . (b,a) by A20, FUNCT_2:26 ; :: 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;

H2 = J1 /\ H by A15, A11;
hence ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) by A14, A13, A17, Th1; :: thesis: verum

end;

A25: len R = len F by A6, FINSEQ_1:def 3;
A26: len R > 0 by A1, A6, FINSEQ_1:def 3;
A27: R . 1 = (Omega). H

proof

1 <= len R by A26, NAT_1:14;
then 1 in Seg (len F) by A25, FINSEQ_1:1;
then ex I being strict Subgroup of G st
( I = F . 1 & R . 1 = I /\ H ) by A6;
hence R . 1 = (Omega). H by A2, GROUP_2:86; :: 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 ) ) ) )
R . (len R) = (1). H

proof

ex I being strict Subgroup of G st
( I = F . (len R) & R . (len R) = I /\ H ) by A1, A6, A25, FINSEQ_1:3;
hence R . (len R) = (1). G by A3, A25, GROUP_2:85
.= (1). H by GROUP_2:63 ;
:: thesis: verum

end;

hence ( 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, A6, A27, A7, FINSEQ_1:def 3; :: thesis: verum