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

now :: thesis: for x being object st x in A holds
x in the carrier of G

let x be object ; :: 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 G st
( x = g & f . g in H99 ) ;
hence x in the carrier of G ; :: thesis: verum

end;

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

A3: now :: thesis: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A

let g1, g2 be Element of G; :: 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 G such that
A6: b = g2 and
A7: f . b in H99 by A5;
consider a being Element of G such that
A8: a = g1 and
A9: f . a in H99 by A4;
set fb = f . b;
set fa = f . a;
( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A9, A7, GROUP_2:50, GROUP_6:def 6;
hence g1 * g2 in A by A8, A6; :: thesis: verum

end;

A10: now :: thesis: for o being Element of O
for g being Element of G st g in A holds
(G ^ o) . g in A

let o be Element of O; :: thesis: for g being Element of G st g in A holds
(G ^ o) . g in A
let g be Element of G; :: 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 G such that
A11: a = g and
A12: f . a in H99 ;
f . a in the carrier of H99 by A12, STRUCT_0:def 5;
then f . a in H9 by STRUCT_0:def 5;
then (H ^ o) . (f . g) in H9 by A11, Lm9;
then f . ((G ^ o) . g) in H9 by Def18;
then f . ((G ^ o) . g) in the carrier of H9 by STRUCT_0:def 5;
then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;
hence (G ^ o) . g in A ; :: thesis: verum

end;

now :: thesis: for g being Element of G st g in A holds
g " in A

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

end;

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

now :: thesis: for g being Element of G holds
( ( g in A implies g in f " the carrier of H9 ) & ( g in f " the carrier of H9 implies g in A ) )

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

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

assume g in A ; :: thesis: g in f " the carrier of H9
then ex a being Element of G st
( a = g & f . a in H99 ) ;
then A16: f . g in the carrier of H9 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:1;
hence g in f " the carrier of H9 by A16, RELSET_1:30; :: thesis: verum

end;

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

end;

hence the carrier of G99 = f " the carrier of H9 by A15, SUBSET_1:3; :: thesis: ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )
reconsider G9 = multMagma(# the carrier of G99, the multF of G99 #) as strict Subgroup of G by Lm15;

now :: thesis: ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )

assume A18: H9 is normal ; :: thesis: ( N is normal StableSubgroup of G99 & G99 is normal )

now :: thesis: for g being Element of G st g in N holds
g in G99

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

end;

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

now :: thesis: for g being Element of G holds g * G9 c= G9 * g

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

now :: thesis: for x being object st x in g * G9 holds
x in G9 * g

H99 is normal by A18;
then A19: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;
let x be object ; :: thesis: ( x in g * G9 implies x in G9 * g )
assume x in g * G9 ; :: thesis: x in G9 * g
then consider h being Element of G such that
A20: x = g * h and
A21: h in A by A15, GROUP_2:27;
set h9 = (g * h) * (g ");
A22: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6
.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6
.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13
.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;
ex a being Element of G st
( a = h & f . a in H99 ) by A21;
then f . ((g * h) * (g ")) in H99 by A19, A22, GROUP_3:58;
then A23: (g * h) * (g ") in A ;
((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3
.= (g * h) * (1_ G) by GROUP_1:def 5
.= x by A20, GROUP_1:def 4 ;
hence x in G9 * g by A15, A23, GROUP_2:28; :: thesis: verum

end;

hence g * G9 c= G9 * g ; :: thesis: verum

end;

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

end;

hence ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) ) ; :: thesis: verum