let G, H be strict Group; :: thesis: for h being Homomorphism of G,H st G is solvable Group holds
Image h is solvable
let h be Homomorphism of G,H; :: thesis: ( G is solvable Group implies Image h is solvable )
assume G is solvable Group ; :: thesis: Image h is solvable
then 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;
1 <= len F by A1, NAT_1:14;
then A5: 1 in Seg (len F) by FINSEQ_1:1;
defpred S₁[ set , set ] means ex J being strict Subgroup of G st
( J = F . $1 & $2 = h .: J );
A6: for k being Nat st k in Seg (len F) holds
ex x being Element of Subgroups (Image h) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of Subgroups (Image h) st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of Subgroups (Image 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 F . k is strict Subgroup of G by GROUP_3:def 1;
then consider A being strict Subgroup of G such that
A7: A = F . k ;
h .: A is strict Subgroup of Image h by Th9;
then h .: A in Subgroups (Image h) by GROUP_3:def 1;
hence ex x being Element of Subgroups (Image h) st S₁[k,x] by A7; :: thesis: verum

end;

consider z being FinSequence of Subgroups (Image h) such that
A8: ( dom z = Seg (len F) & ( for j being Nat st j in Seg (len F) holds
S₁[j,z . j] ) ) from FINSEQ_1:sch 5(A6);
Seg (len z) = Seg (len F) by A8, FINSEQ_1:def 3;
then A9: dom F = Seg (len z) by FINSEQ_1:def 3
.= dom z by FINSEQ_1:def 3 ;
A10: for i being Element of NAT st i in dom z & i + 1 in dom z holds
for G1, G2 being strict Subgroup of Image h st G1 = z . i & G2 = z . (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 ) )

proof

let i be Element of NAT ; :: thesis: ( i in dom z & i + 1 in dom z implies for G1, G2 being strict Subgroup of Image h st G1 = z . i & G2 = z . (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 ) ) )
assume that
A11: i in dom z and
A12: i + 1 in dom z ; :: thesis: for G1, G2 being strict Subgroup of Image h st G1 = z . i & G2 = z . (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 ) )
let G1, G2 be strict Subgroup of Image h; :: thesis: ( G1 = z . i & G2 = z . (i + 1) implies ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume that
A13: G1 = z . i and
A14: G2 = z . (i + 1) ; :: thesis: ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
consider A being strict Subgroup of G such that
A15: A = F . i and
A16: G1 = h .: A by A8, A11, A13;
consider B being strict Subgroup of G such that
A17: B = F . (i + 1) and
A18: G2 = h .: B by A8, A12, A14;
A19: for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative

proof

let N be normal Subgroup of G1; :: thesis: ( N = G2 implies G1 ./. N is commutative )
assume A20: N = G2 ; :: thesis: G1 ./. N is commutative

now :: thesis: for x, y being Element of (G1 ./. N) holds x * y = y * x

let x, y be Element of (G1 ./. N); :: thesis: x * y = y * x
x in G1 ./. N by STRUCT_0:def 5;
then consider a being Element of G1 such that
A21: x = a * N and
x = N * a by GROUP_6:23;
y in G1 ./. N by STRUCT_0:def 5;
then consider b being Element of G1 such that
A22: y = b * N and
y = N * b by GROUP_6:23;
x in the carrier of (G1 ./. N) ;
then A23: x in Cosets N by GROUP_6:17;
then reconsider x1 = x as Subset of G1 ;
b in h .: A by A16, STRUCT_0:def 5;
then consider b1 being Element of A such that
A24: b = (h | A) . b1 by GROUP_6:45;
reconsider b1 = b1 as Element of G by GROUP_2:42;
b = h . b1 by A24, FUNCT_1:49;
then A25: b * N = (h . b1) * (h .: B) by A18, A20, GROUP_6:2
.= h .: (b1 * B) by Th13 ;
then reconsider y2 = h .: (b1 * B) as Subset of G1 ;
a in h .: A by A16, STRUCT_0:def 5;
then consider a1 being Element of A such that
A26: a = (h | A) . a1 by GROUP_6:45;
reconsider a1 = a1 as Element of G by GROUP_2:42;
a = h . a1 by A26, FUNCT_1:49;
then A27: a * N = (h . a1) * (h .: B) by A18, A20, GROUP_6:2
.= h .: (a1 * B) by Th13 ;
then reconsider x2 = h .: (a1 * B) as Subset of G1 ;

now :: thesis: for z being object st z in x2 * y2 holds
z in (h .: (a1 * B)) * (h .: (b1 * B))

let z be object ; :: thesis: ( z in x2 * y2 implies z in (h .: (a1 * B)) * (h .: (b1 * B)) )
assume z in x2 * y2 ; :: thesis: z in (h .: (a1 * B)) * (h .: (b1 * B))
then consider z1, z2 being Element of G1 such that
A28: z = z1 * z2 and
A29: z1 in x2 and
A30: z2 in y2 ;
reconsider z22 = z2 as Element of H by A30;
reconsider z11 = z1 as Element of H by A29;
z = z11 * z22 by A28, GROUP_2:43;
hence z in (h .: (a1 * B)) * (h .: (b1 * B)) by A29, A30; :: thesis: verum

end;

then A31: x2 * y2 c= (h .: (a1 * B)) * (h .: (b1 * B)) ;
A32: (a1 * B) * (b1 * B) = (b1 * B) * (a1 * B)

proof

reconsider K = B as normal Subgroup of A by A4, A9, A11, A12, A15, A17;
reconsider a2 = a1, b2 = b1 as Element of A ;
A33: a1 * B = a2 * K by GROUP_6:2;
then reconsider A1 = a1 * B as Subset of A ;
A34: b1 * B = b2 * K by GROUP_6:2;
then reconsider B1 = b1 * B as Subset of A ;
reconsider a12 = a1 * B, b12 = b1 * B as Element of Cosets K by A33, A34, GROUP_6:14;
a2 * K is Element of (A ./. K) by GROUP_6:22;
then reconsider a11 = a12 as Element of (A ./. K) by GROUP_6:2;
b2 * K is Element of (A ./. K) by GROUP_6:22;
then reconsider b11 = b12 as Element of (A ./. K) by GROUP_6:2;

now :: thesis: for x being object st x in (a1 * B) * (b1 * B) holds
x in A1 * B1

let x be object ; :: thesis: ( x in (a1 * B) * (b1 * B) implies x in A1 * B1 )
assume x in (a1 * B) * (b1 * B) ; :: thesis: x in A1 * B1
then consider z1, z2 being Element of G such that
A35: x = z1 * z2 and
A36: ( z1 in a1 * B & z2 in b1 * B ) ;
( z1 in A1 & z2 in B1 ) by A36;
then reconsider z11 = z1, z22 = z2 as Element of A ;
z1 * z2 = z11 * z22 by GROUP_2:43;
hence x in A1 * B1 by A35, A36; :: thesis: verum

end;

then A37: (a1 * B) * (b1 * B) c= A1 * B1 ;

now :: thesis: for x being object st x in (b1 * B) * (a1 * B) holds
x in B1 * A1

let x be object ; :: thesis: ( x in (b1 * B) * (a1 * B) implies x in B1 * A1 )
assume x in (b1 * B) * (a1 * B) ; :: thesis: x in B1 * A1
then consider z1, z2 being Element of G such that
A38: x = z1 * z2 and
A39: ( z1 in b1 * B & z2 in a1 * B ) ;
( z1 in B1 & z2 in A1 ) by A39;
then reconsider z11 = z1, z22 = z2 as Element of A ;
z1 * z2 = z11 * z22 by GROUP_2:43;
hence x in B1 * A1 by A38, A39; :: thesis: verum

end;

then A40: (b1 * B) * (a1 * B) c= B1 * A1 ;

now :: thesis: for x being object st x in B1 * A1 holds
x in (b1 * B) * (a1 * B)

let x be object ; :: thesis: ( x in B1 * A1 implies x in (b1 * B) * (a1 * B) )
assume x in B1 * A1 ; :: thesis: x in (b1 * B) * (a1 * B)
then consider z1, z2 being Element of A such that
A41: x = z1 * z2 and
A42: ( z1 in B1 & z2 in A1 ) ;
reconsider z11 = z1, z22 = z2 as Element of G by A42;
z1 * z2 = z11 * z22 by GROUP_2:43;
hence x in (b1 * B) * (a1 * B) by A41, A42; :: thesis: verum

end;

then A43: B1 * A1 c= (b1 * B) * (a1 * B) ;
A44: A ./. K is commutative Group by A4, A9, A11, A12, A15, A17;
A45: for a, b being Element of (A ./. K) holds the multF of (A ./. K) . (a,b) = the multF of (A ./. K) . (b,a) by A44, BINOP_1:def 2, GROUP_3:2;
A46: A1 * B1 = (CosOp K) . (a11,b11) by GROUP_6:def 3
.= the multF of (A ./. K) . (a12,b12) by GROUP_6:18
.= the multF of (A ./. K) . (b11,a11) by A45
.= (CosOp K) . (b12,a12) by GROUP_6:18
.= B1 * A1 by GROUP_6:def 3 ;

now :: thesis: for x being object st x in A1 * B1 holds
x in (a1 * B) * (b1 * B)

let x be object ; :: thesis: ( x in A1 * B1 implies x in (a1 * B) * (b1 * B) )
assume x in A1 * B1 ; :: thesis: x in (a1 * B) * (b1 * B)
then consider z1, z2 being Element of A such that
A47: x = z1 * z2 and
A48: ( z1 in A1 & z2 in B1 ) ;
reconsider z11 = z1, z22 = z2 as Element of G by A48;
z1 * z2 = z11 * z22 by GROUP_2:43;
hence x in (a1 * B) * (b1 * B) by A47, A48; :: thesis: verum

end;

then A1 * B1 c= (a1 * B) * (b1 * B) ;
then (a1 * B) * (b1 * B) = A1 * B1 by A37, XBOOLE_0:def 10;
hence (a1 * B) * (b1 * B) = (b1 * B) * (a1 * B) by A46, A40, A43, XBOOLE_0:def 10; :: thesis: verum

end;

now :: thesis: for z being object st z in y2 * x2 holds
z in (h .: (b1 * B)) * (h .: (a1 * B))

let z be object ; :: thesis: ( z in y2 * x2 implies z in (h .: (b1 * B)) * (h .: (a1 * B)) )
assume z in y2 * x2 ; :: thesis: z in (h .: (b1 * B)) * (h .: (a1 * B))
then consider z1, z2 being Element of G1 such that
A49: z = z1 * z2 and
A50: z1 in y2 and
A51: z2 in x2 ;
reconsider z22 = z2 as Element of H by A51;
reconsider z11 = z1 as Element of H by A50;
z = z11 * z22 by A49, GROUP_2:43;
hence z in (h .: (b1 * B)) * (h .: (a1 * B)) by A50, A51; :: thesis: verum

end;

then A52: y2 * x2 c= (h .: (b1 * B)) * (h .: (a1 * B)) ;
A53: (h .: (b1 * B)) * (h .: (a1 * B)) = h .: ((b1 * B) * (a1 * B)) by Th14;

now :: thesis: for z being object st z in (h .: (b1 * B)) * (h .: (a1 * B)) holds
z in y2 * x2

let z be object ; :: thesis: ( z in (h .: (b1 * B)) * (h .: (a1 * B)) implies z in y2 * x2 )
assume z in (h .: (b1 * B)) * (h .: (a1 * B)) ; :: thesis: z in y2 * x2
then consider x being object such that
A54: x in the carrier of G and
A55: x in (b1 * B) * (a1 * B) and
A56: z = h . x by A53, FUNCT_2:64;
reconsider x = x as Element of G by A54;
consider z1, z2 being Element of G such that
A57: x = z1 * z2 and
A58: z1 in b1 * B and
A59: z2 in a1 * B by A55;
A60: h . z2 in x2 by A59, FUNCT_2:35;
then reconsider z22 = h . z2 as Element of G1 ;
A61: h . z1 in y2 by A58, FUNCT_2:35;
then reconsider z11 = h . z1 as Element of G1 ;
z = (h . z1) * (h . z2) by A56, A57, GROUP_6:def 6
.= z11 * z22 by GROUP_2:43 ;
hence z in y2 * x2 by A61, A60; :: thesis: verum

end;

then (h .: (b1 * B)) * (h .: (a1 * B)) c= y2 * x2 ;
then A62: y2 * x2 = (h .: (b1 * B)) * (h .: (a1 * B)) by A52, XBOOLE_0:def 10;
A63: (h .: (a1 * B)) * (h .: (b1 * B)) = h .: ((a1 * B) * (b1 * B)) by Th14;

now :: thesis: for z being object st z in (h .: (a1 * B)) * (h .: (b1 * B)) holds
z in x2 * y2

let z be object ; :: thesis: ( z in (h .: (a1 * B)) * (h .: (b1 * B)) implies z in x2 * y2 )
assume z in (h .: (a1 * B)) * (h .: (b1 * B)) ; :: thesis: z in x2 * y2
then consider x being object such that
A64: x in the carrier of G and
A65: x in (a1 * B) * (b1 * B) and
A66: z = h . x by A63, FUNCT_2:64;
reconsider x = x as Element of G by A64;
consider z1, z2 being Element of G such that
A67: x = z1 * z2 and
A68: z1 in a1 * B and
A69: z2 in b1 * B by A65;
A70: h . z2 in y2 by A69, FUNCT_2:35;
then reconsider z22 = h . z2 as Element of G1 ;
A71: h . z1 in x2 by A68, FUNCT_2:35;
then reconsider z11 = h . z1 as Element of G1 ;
z = (h . z1) * (h . z2) by A66, A67, GROUP_6:def 6
.= z11 * z22 by GROUP_2:43 ;
hence z in x2 * y2 by A71, A70; :: thesis: verum

end;

then (h .: (a1 * B)) * (h .: (b1 * B)) c= x2 * y2 ;
then A72: x2 * y2 = (h .: (a1 * B)) * (h .: (b1 * B)) by A31, XBOOLE_0:def 10;
y in the carrier of (G1 ./. N) ;
then A73: y in Cosets N by GROUP_6:17;
then reconsider y1 = y as Subset of G1 ;
thus x * y = (CosOp N) . (x,y) by GROUP_6:18
.= y1 * x1 by A23, A73, A21, A22, A27, A25, A63, A72, A53, A62, A32, GROUP_6:def 3
.= (CosOp N) . (y,x) by A23, A73, GROUP_6:def 3
.= y * x by GROUP_6:18 ; :: thesis: verum

end;

hence G1 ./. N is commutative by GROUP_1:def 12; :: thesis: verum

end;

B is strict normal Subgroup of A by A4, A9, A11, A12, A15, A17;
hence ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) by A16, A18, A19, Th15; :: thesis: verum

end;

take z ; :: according to GRSOLV_1:def 1 :: thesis: ( len z > 0 & z . 1 = (Omega). (Image h) & z . (len z) = (1). (Image h) & ( for i being Element of NAT st i in dom z & i + 1 in dom z holds
for G1, G2 being strict Subgroup of Image h st G1 = z . i & G2 = z . (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 ) ) ) )
A74: len z = len F by A8, FINSEQ_1:def 3;
( z . 1 = (Omega). (Image h) & z . (len z) = (1). (Image h) )

proof

ex A being strict Subgroup of G st
( A = F . 1 & z . 1 = h .: A ) by A8, A5;
hence z . 1 = (Omega). (Image h) by A2, Th11; :: thesis: z . (len z) = (1). (Image h)
ex B being strict Subgroup of G st
( B = F . (len F) & z . (len F) = h .: B ) by A1, A8, FINSEQ_1:3;
hence z . (len z) = (1). H by A3, A74, Th11
.= (1). (Image h) by GROUP_2:63 ;
:: thesis: verum

end;

hence ( len z > 0 & z . 1 = (Omega). (Image h) & z . (len z) = (1). (Image h) & ( for i being Element of NAT st i in dom z & i + 1 in dom z holds
for G1, G2 being strict Subgroup of Image h st G1 = z . i & G2 = z . (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, A8, A10, FINSEQ_1:def 3; :: thesis: verum