let O be set ; 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; 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; 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; 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; ( 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
; 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 ;
then reconsider A = A as Subset of G by TARSKI:def 3;
then consider G99 being strict StableSubgroup of G such that
A15:
the carrier of G99 = A
by A3, A10, Lm14;
take
G99
; ( the carrier of G99 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) ) )
hence
the carrier of G99 = f " the carrier of H9
by A15, SUBSET_1:3; ( 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;
hence
( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )
; verum