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

now

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

end;

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

A4: now

let g1, g2 be Element of G; :: thesis:
assume A5: ( g1 in A & g2 in A ) ; :: thesis:
then consider a being Element of G such that
A6: ( a = g1 & f . a in H'' ) ;
consider b being Element of G such that
A7: ( b = g2 & f . b in H'' ) by A5;
A8: f . (a * b) = (f . a) * (f . b) by GROUP_6:def 7;
set fa = f . a;
set fb = f . b;
(f . a) * (f . b) in H'' by A6, A7, GROUP_2:59;
hence g1 * g2 in A by A6, A7, A8; :: thesis:

end;

A9: now

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

end;

now

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

end;

then consider G'' being strict StableSubgroup of G such that
A12: the carrier of G'' = A by A4, A9, Lm15;
reconsider G' = multMagma(# the carrier of G'',the multF of G'' #) as strict Subgroup of G by Lm16;
take G'' ; :: thesis:

now

let g be Element of G; :: thesis:
reconsider R = f as Relation of the carrier of G,the carrier of H ;

hereby :: thesis:

assume g in A ; :: thesis:
then consider a being Element of G such that
A13: ( a = g & f . a in H'' ) ;
dom f = the carrier of G by FUNCT_2:def 1;
then A14: [g,(f . g)] in f by FUNCT_1:8;
f . g in the carrier of H' by A13, STRUCT_0:def 5;
hence g in f " the carrier of H' by A14, RELSET_1:53; :: thesis:

end;

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

end;

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

now

assume A17: H' is normal ; :: thesis:

now

let g be Element of G; :: thesis:
assume g in N ; :: thesis:
then f . g = 1_ H by A1, Th47;
then g in the carrier of G'' by A2, A12;
hence g in G'' by STRUCT_0:def 5; :: thesis:

end;

hence N is normal StableSubgroup of G'' by A1, Th13, Th40; :: thesis:

now

let g be Element of G; :: thesis:

now

let x be set ; :: thesis:
assume x in g * G' ; :: thesis:
then consider h being Element of G such that
A18: ( x = g * h & h in A ) by A12, GROUP_2:33;
consider a being Element of G such that
A19: ( a = h & f . a in H'' ) by A18;
set h' = (g * h) * (g " );
A20: ((g * h) * (g " )) * g = (g * h) * ((g " ) * g) by GROUP_1:def 4
.= (g * h) * (1_ G) by GROUP_1:def 6
.= x by A18, GROUP_1:def 5 ;
H'' is normal by A17, Def10;
then A21: H'' |^ ((f . g) " ) = H'' by GROUP_3:def 13;
f . ((g * h) * (g " )) = (f . (g * h)) * (f . (g " )) by GROUP_6:def 7
.= ((f . g) * (f . h)) * (f . (g " )) by GROUP_6:def 7
.= ((f . g) * (f . h)) * ((f . g) " ) by Lm14
.= ((((f . g) " ) " ) * (f . h)) * ((f . g) " )
.= (f . h) |^ ((f . g) " ) by GROUP_3:def 2 ;
then f . ((g * h) * (g " )) in H'' by A19, A21, GROUP_3:70;
then (g * h) * (g " ) in A ;
hence x in G' * g by A12, A20, GROUP_2:34; :: thesis:

end;

hence g * G' c= G' * g by TARSKI:def 3; :: thesis:

end;

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

end;

hence ( H' is normal implies ( N is normal StableSubgroup of G'' & G'' is normal ) ) ; :: thesis: