let O be set ; :: thesis: for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for H' being strict StableSubgroup of H
for f being Homomorphism of G,H st N = Ker f holds
ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) )
let G, H be GroupWithOperators of O; :: thesis: for N being StableSubgroup of G
for H' being strict StableSubgroup of H
for f being Homomorphism of G,H st N = Ker f holds
ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) )
let N be StableSubgroup of G; :: thesis: for H' being strict StableSubgroup of H
for f being Homomorphism of G,H st N = Ker f holds
ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) )
let H' be strict StableSubgroup of H; :: thesis: for f being Homomorphism of G,H st N = Ker f holds
ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) )
reconsider H'' = multMagma(# the carrier of H',the multF of H' #) as strict Subgroup of H by Lm16;
let f be Homomorphism of G,H; :: thesis: ( N = Ker f implies ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) ) )
assume A1: N = Ker f ; :: thesis: ex G' being strict StableSubgroup of G st
( the carrier of G' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G' & G' is normal ) ) )
set A = { g where g is Element of : 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 : f . g in H'' } ;
then reconsider A = { g where g is Element of : f . g in H'' } as non empty set ;

now

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

end;

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

A3: now

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

end;

A10: now

let o be Element of O; :: thesis: for g being Element of st g in A holds
(G ^ o) . g in A
let g be Element of ; :: thesis: ( g in A implies (G ^ o) . g in A )
assume g in A ; :: thesis: (G ^ o) . g in A
then consider a being Element of such that
A11: a = g and
A12: f . a in H'' ;
f . a in the carrier of H'' by A12, 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: verum

end;

now

let g be Element of ; :: thesis: ( g in A implies g " in A )
assume g in A ; :: thesis: g " in A
then consider a being Element of such that
A13: a = g and
A14: f . a in H'' ;
(f . a) " in H'' by A14, GROUP_2:60;
then f . (a " ) in H'' by Lm14;
hence g " in A by A13; :: thesis: verum

end;

then consider G'' being strict StableSubgroup of G such that
A15: the carrier of G'' = A by A3, A10, Lm15;
take G'' ; :: thesis: ( the carrier of G'' = f " the carrier of H' & ( H' is normal implies ( N is normal StableSubgroup of G'' & G'' is normal ) ) )

now

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

hereby :: thesis: ( g in f " the carrier of H' implies g in A )

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

end;

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

end;

hence the carrier of G'' = f " the carrier of H' by A15, SUBSET_1:8; :: thesis: ( H' is normal implies ( N is normal StableSubgroup of G'' & G'' is normal ) )
reconsider G' = multMagma(# the carrier of G'',the multF of G'' #) as strict Subgroup of G by Lm16;

now

assume A18: H' is normal ; :: thesis: ( N is normal StableSubgroup of G'' & G'' is normal )

now

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

end;

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

now

let g be Element of ; :: thesis: g * G' c= G' * g

now

H'' is normal by A18, Def10;
then A19: H'' |^ ((f . g) " ) = H'' by GROUP_3:def 13;
let x be set ; :: thesis: ( x in g * G' implies x in G' * g )
assume x in g * G' ; :: thesis: x in G' * g
then consider h being Element of such that
A20: x = g * h and
A21: h in A by A15, GROUP_2:33;
set h' = (g * h) * (g " );
A22: 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 ;
ex a being Element of st
( a = h & f . a in H'' ) by A21;
then f . ((g * h) * (g " )) in H'' by A19, A22, GROUP_3:70;
then A23: (g * h) * (g " ) in A ;
((g * h) * (g " )) * g = (g * h) * ((g " ) * g) by GROUP_1:def 4
.= (g * h) * (1_ G) by GROUP_1:def 6
.= x by A20, GROUP_1:def 5 ;
hence x in G' * g by A15, A23, GROUP_2:34; :: thesis: verum

end;

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

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: verum

end;

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