let O be set ; :: thesis:
let G, H be GroupWithOperators of O; :: thesis:
let N be StableSubgroup of G; :: thesis:
reconsider N' = multMagma(# the carrier of N,the multF of N #) as strict Subgroup of G by Lm16;
let G' be strict StableSubgroup of G; :: thesis:
reconsider G'' = multMagma(# the carrier of G',the multF of G' #) as strict Subgroup of G by Lm16;
let f be Homomorphism of G,H; :: thesis:
set A = { (f . g) where g is Element of : g in G'' } ;
A1: ( G'' * N' = G' * N & N' * G'' = N * G' ) ;
1_ G in G'' by GROUP_2:55;
then f . (1_ G) in { (f . g) where g is Element of : g in G'' } ;
then reconsider A = { (f . g) where g is Element of : g in G'' } as non empty set ;

now

let x be set ; :: thesis:
assume x in A ; :: thesis:
then ex g being Element of st
( x = f . g & g in G'' ) ;
hence x in the carrier of H ; :: thesis:

end;

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

A2: now

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

end;

A7: now

let o be Element of O; :: thesis:
let h be Element of ; :: thesis:
assume h in A ; :: thesis:
then consider g being Element of such that
A8: h = f . g and
A9: g in G'' ;
g in the carrier of G'' by A9, 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 A10: (G ^ o) . g in G'' by STRUCT_0:def 5;
(H ^ o) . h = f . ((G ^ o) . g) by A8, Def18;
hence (H ^ o) . h in A by A10; :: thesis:

end;

now

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

end;

then consider H'' being strict StableSubgroup of H such that
A12: the carrier of H'' = A by A2, A7, Lm15;
assume A13: N = Ker f ; :: thesis:
then N' is normal by Def10;
then A14: (carr G'') * N' = N' * (carr G'') by GROUP_3:143;
reconsider H' = multMagma(# the carrier of H'',the multF of H'' #) as strict Subgroup of H by Lm16;
take H'' ; :: thesis:

A15: now

reconsider R = f as Relation of , ;
let h be Element of ; :: thesis:

hereby :: thesis:

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

end;

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

end;

hence A20: the carrier of H'' = f .: the carrier of G' by A12, SUBSET_1:8; :: thesis:

A21: now

let x be set ; :: thesis:
assume A22: x in f " the carrier of H' ; :: thesis:
then f . x in the carrier of H' by FUNCT_1:def 13;
then consider g1 being set such that
A23: g1 in dom f and
A24: g1 in the carrier of G' and
A25: f . g1 = f . x by A20, FUNCT_1:def 12;
reconsider g1 = g1, g2 = x as Element of by A22, A23;
consider g3 being Element of such that
A26: g2 = g1 * g3 by GROUP_1:23;
f . g2 = (f . g2) * (f . g3) by A25, A26, 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 A13, STRUCT_0:def 5;
hence x in G'' * N' by A24, A26; :: thesis:

end;

A27: dom f = the carrier of G by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume A28: x in G'' * N' ; :: thesis:
then consider g1, g2 being Element of such that
A29: x = g1 * g2 and
A30: g1 in carr G' and
A31: g2 in carr N' ;
A32: g2 in Ker f by A13, A31, STRUCT_0:def 5;
f . x = (f . g1) * (f . g2) by A29, GROUP_6:def 7
.= (f . g1) * (1_ H) by A32, Th47
.= f . g1 by GROUP_1:def 5 ;
then f . x in f .: the carrier of G' by A27, A30, FUNCT_1:def 12;
then x in f " (f .: the carrier of G') by A27, A28, FUNCT_1:def 13;
hence x in f " the carrier of H' by A12, A15, SUBSET_1:8; :: thesis:

end;

then f " the carrier of H' = (carr G') * (carr N) by A21, TARSKI:2;
hence f " the carrier of H'' = the carrier of (G' "\/" N) by A14, A1, Th30; :: thesis:

now

assume that
A33: f is onto and
A34: G' is normal ; :: thesis:
A35: G'' is normal by A34, Def10;

now

let h1 be Element of ; :: thesis:

now

let x be set ; :: thesis:
assume x in h1 * H' ; :: thesis:
then consider h2 being Element of such that
A36: x = h1 * h2 and
A37: h2 in A by A12, GROUP_2:33;
set h2' = (h1 * h2) * (h1 " );
h2 in f .: the carrier of G' by A15, A37;
then consider g2 being set such that
A38: g2 in dom f and
A39: g2 in the carrier of G'' and
A40: f . g2 = h2 by FUNCT_1:def 12;
rng f = the carrier of H by A33, FUNCT_2:def 3;
then consider g1 being set such that
A41: g1 in dom f and
A42: h1 = f . g1 by FUNCT_1:def 5;
reconsider g1 = g1, g2 = g2 as Element of by A38, A41;
set g2' = (g1 * g2) * (g1 " );
(g1 * g2) * (g1 " ) = (((g1 " ) " ) * g2) * (g1 " ) ;
then A43: (g1 * g2) * (g1 " ) = g2 |^ (g1 " ) by GROUP_3:def 2;
g2 in G'' by A39, STRUCT_0:def 5;
then (g1 * g2) * (g1 " ) in G'' |^ (g1 " ) by A43, GROUP_3:70;
then A44: (g1 * g2) * (g1 " ) in the carrier of (G'' |^ (g1 " )) by STRUCT_0:def 5;
G'' |^ (g1 " ) is Subgroup of G'' by A35, GROUP_3:145;
then A45: 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 A40, A42, 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 A27, A44, A45, FUNCT_1:def 12;
then A46: (h1 * h2) * (h1 " ) in A by A15;
((h1 * h2) * (h1 " )) * h1 = (h1 * h2) * ((h1 " ) * h1) by GROUP_1:def 4
.= (h1 * h2) * (1_ H) by GROUP_1:def 6
.= x by A36, GROUP_1:def 5 ;
hence x in H' * h1 by A12, A46, GROUP_2:34; :: thesis:

end;

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

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:

end;

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