let O be set ; :: thesis: for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for G' being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) )
let G, H be GroupWithOperators of O; :: thesis: for N being StableSubgroup of G
for G' being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) )
let N be StableSubgroup of G; :: thesis: for G' being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) )
let G' be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H st N = Ker f holds
ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) )
let f be Homomorphism of G,H; :: thesis: ( N = Ker f implies ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) ) )
assume A1: N = Ker f ; :: thesis: ex H' being strict StableSubgroup of H st
( the carrier of H' = f .: the carrier of G' & f " the carrier of H' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H' is normal ) )
reconsider G'' = multMagma(# the carrier of G',the multF of G' #) as strict Subgroup of G by Lm16;
set A = { (f . g) where g is Element of G : g in G'' } ;
1_ G in G'' by GROUP_2:55;
then f . (1_ G) in { (f . g) where g is Element of G : g in G'' } ;
then reconsider A = { (f . g) where g is Element of G : g in G'' } as non empty set ;

now

let x be set ; :: thesis: ( x in A implies x in the carrier of H )
assume x in A ; :: thesis: x in the carrier of H
then consider g being Element of G such that
A2: ( x = f . g & g in G'' ) ;
thus x in the carrier of H by A2; :: thesis: verum

end;

then reconsider A = A as Subset of H by TARSKI:def 3;

A3: now

let h1, h2 be Element of H; :: thesis: ( h1 in A & h2 in A implies h1 * h2 in A )
assume A4: ( h1 in A & h2 in A ) ; :: thesis: h1 * h2 in A
then consider a being Element of G such that
A5: ( h1 = f . a & a in G'' ) ;
consider b being Element of G such that
A6: ( h2 = f . b & b in G'' ) by A4;
A7: f . (a * b) = h1 * h2 by A5, A6, GROUP_6:def 7;
a * b in G'' by A5, A6, GROUP_2:59;
hence h1 * h2 in A by A7; :: thesis: verum

end;

A8: now

let h be Element of H; :: thesis: ( h in A implies h " in A )
assume h in A ; :: thesis: h " in A
then consider g being Element of G such that
A9: ( h = f . g & g in G'' ) ;
A10: g " in G'' by A9, GROUP_2:60;
h " = f . (g " ) by A9, Lm14;
hence h " in A by A10; :: thesis: verum

end;

now

let o be Element of O; :: thesis: for h being Element of H st h in A holds
(H ^ o) . h in A
let h be Element of H; :: thesis: ( h in A implies (H ^ o) . h in A )
assume h in A ; :: thesis: (H ^ o) . h in A
then consider g being Element of G such that
A11: ( h = f . g & g in G'' ) ;
A12: (H ^ o) . h = f . ((G ^ o) . g) by A11, Def18;
g in the carrier of G'' by A11, STRUCT_0:def 5;
then g in G' by STRUCT_0:def 5;
then (G ^ o) . g in G' by Lm10;
then (G ^ o) . g in the carrier of G' by STRUCT_0:def 5;
then (G ^ o) . g in G'' by STRUCT_0:def 5;
hence (H ^ o) . h in A by A12; :: thesis: verum

end;

then consider H'' being strict StableSubgroup of H such that
A13: the carrier of H'' = A by A3, A8, Lm15;
reconsider H' = multMagma(# the carrier of H'',the multF of H'' #) as strict Subgroup of H by Lm16;
take H'' ; :: thesis: ( the carrier of H'' = f .: the carrier of G' & f " the carrier of H'' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H'' is normal ) )

A14: now

let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G' ) & ( h in f .: the carrier of G' implies h in A ) )
reconsider R = f as Relation of the carrier of G,the carrier of H ;

hereby :: thesis: ( h in f .: the carrier of G' implies h in A )

assume h in A ; :: thesis: h in f .: the carrier of G'
then consider g being Element of G such that
A15: ( h = f . g & g in G'' ) ;
dom f = the carrier of G by FUNCT_2:def 1;
then A16: [g,h] in f by A15, FUNCT_1:8;
g in the carrier of G' by A15, STRUCT_0:def 5;
hence h in f .: the carrier of G' by A16, RELSET_1:52; :: thesis: verum

end;

assume h in f .: the carrier of G' ; :: thesis: h in A
then consider g being Element of G such that
A17: ( [g,h] in R & g in the carrier of G' ) by RELSET_1:52;
A18: f . g = h by A17, FUNCT_1:8;
g in G'' by A17, STRUCT_0:def 5;
hence h in A by A18; :: thesis: verum

end;

hence A19: the carrier of H'' = f .: the carrier of G' by A13, SUBSET_1:8; :: thesis: ( f " the carrier of H'' = the carrier of (G' "\/" N) & ( f is onto & G' is normal implies H'' is normal ) )
reconsider N' = multMagma(# the carrier of N,the multF of N #) as strict Subgroup of G by Lm16;
N' is normal by A1, Def10;
then A20: (carr G'') * N' = N' * (carr G'') by GROUP_3:143;
A21: dom f = the carrier of G by FUNCT_2:def 1;

A22: now

let x be set ; :: thesis: ( x in f " the carrier of H' implies x in G'' * N' )
assume A23: x in f " the carrier of H' ; :: thesis: x in G'' * N'
then ( x in dom f & f . x in the carrier of H' ) by FUNCT_1:def 13;
then consider g1 being set such that
A24: ( g1 in dom f & g1 in the carrier of G' & f . g1 = f . x ) by A19, FUNCT_1:def 12;
reconsider g1 = g1, g2 = x as Element of G by A23, A24;
consider g3 being Element of G such that
A25: g2 = g1 * g3 by GROUP_1:23;
f . g2 = (f . g2) * (f . g3) by A24, A25, GROUP_6:def 7;
then f . g3 = 1_ H by GROUP_1:15;
then g3 in Ker f by Th47;
then g3 in the carrier of N by A1, STRUCT_0:def 5;
hence x in G'' * N' by A24, A25; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in G'' * N' implies x in f " the carrier of H' )
assume A26: x in G'' * N' ; :: thesis: x in f " the carrier of H'
then consider g1, g2 being Element of G such that
A27: ( x = g1 * g2 & g1 in carr G' & g2 in carr N' ) ;
A28: g2 in Ker f by A1, A27, STRUCT_0:def 5;
f . x = (f . g1) * (f . g2) by A27, GROUP_6:def 7
.= (f . g1) * (1_ H) by A28, Th47
.= f . g1 by GROUP_1:def 5 ;
then f . x in f .: the carrier of G' by A21, A27, FUNCT_1:def 12;
then x in f " (f .: the carrier of G') by A21, A26, FUNCT_1:def 13;
hence x in f " the carrier of H' by A13, A14, SUBSET_1:8; :: thesis: verum

end;

then A29: f " the carrier of H' = (carr G') * (carr N) by A22, TARSKI:2;
A30: G'' * N' = G' * N ;
N' * G'' = N * G' ;
hence f " the carrier of H'' = the carrier of (G' "\/" N) by A20, A29, A30, Th30; :: thesis: ( f is onto & G' is normal implies H'' is normal )

now

assume A31: ( f is onto & G' is normal ) ; :: thesis: H'' is normal
then A32: G'' is normal by Def10;

now

let h1 be Element of H; :: thesis: h1 * H' c= H' * h1

now

let x be set ; :: thesis: ( x in h1 * H' implies x in H' * h1 )
assume x in h1 * H' ; :: thesis: x in H' * h1
then consider h2 being Element of H such that
A33: ( x = h1 * h2 & h2 in A ) by A13, GROUP_2:33;
h2 in f .: the carrier of G' by A14, A33;
then consider g2 being set such that
A34: ( g2 in dom f & g2 in the carrier of G'' & f . g2 = h2 ) by FUNCT_1:def 12;
set h2' = (h1 * h2) * (h1 " );
A35: ((h1 * h2) * (h1 " )) * h1 = (h1 * h2) * ((h1 " ) * h1) by GROUP_1:def 4
.= (h1 * h2) * (1_ H) by GROUP_1:def 6
.= x by A33, GROUP_1:def 5 ;
rng f = the carrier of H by A31, FUNCT_2:def 3;
then consider g1 being set such that
A36: ( g1 in dom f & h1 = f . g1 ) by FUNCT_1:def 5;
reconsider g1 = g1, g2 = g2 as Element of G by A34, A36;
set g2' = (g1 * g2) * (g1 " );
(g1 * g2) * (g1 " ) = (((g1 " ) " ) * g2) * (g1 " ) ;
then ( (g1 * g2) * (g1 " ) = g2 |^ (g1 " ) & g2 in G'' ) by A34, GROUP_3:def 2, STRUCT_0:def 5;
then (g1 * g2) * (g1 " ) in G'' |^ (g1 " ) by GROUP_3:70;
then A37: (g1 * g2) * (g1 " ) in the carrier of (G'' |^ (g1 " )) by STRUCT_0:def 5;
G'' |^ (g1 " ) is Subgroup of G'' by A32, GROUP_3:145;
then A38: the carrier of (G'' |^ (g1 " )) c= the carrier of G'' by GROUP_2:def 5;
(h1 * h2) * (h1 " ) = ((f . g1) * (f . g2)) * (f . (g1 " )) by A34, A36, Lm14
.= (f . (g1 * g2)) * (f . (g1 " )) by GROUP_6:def 7
.= f . ((g1 * g2) * (g1 " )) by GROUP_6:def 7 ;
then (h1 * h2) * (h1 " ) in f .: the carrier of G'' by A21, A37, A38, FUNCT_1:def 12;
then (h1 * h2) * (h1 " ) in A by A14;
hence x in H' * h1 by A13, A35, GROUP_2:34; :: thesis: verum

end;

hence h1 * H' c= H' * h1 by TARSKI:def 3; :: thesis: verum

end;

then for H1 being strict Subgroup of H st H1 = multMagma(# the carrier of H'',the multF of H'' #) holds
H1 is normal by GROUP_3:141;
hence H'' is normal by Def10; :: thesis: verum

end;

hence ( f is onto & G' is normal implies H'' is normal ) ; :: thesis: verum