let O be set ; :: thesis: for G being GroupWithOperators of O

for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N

let G be GroupWithOperators of O; :: thesis: for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N

let N be strict normal StableSubgroup of G; :: thesis: Ker (nat_hom N) = N

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;

A1: ( nat_hom N = nat_hom N9 & 1_ (G ./. N) = 1_ (G ./. N9) ) by Def20, Lm34;

the carrier of (Ker (nat_hom N)) = { a where a is Element of G : (nat_hom N) . a = 1_ (G ./. N) } by Def21

.= { a where a is Element of G : (nat_hom N9) . a = 1_ (G ./. N9) } by A1

.= the carrier of (Ker (nat_hom N9)) by GROUP_6:def 9

.= the carrier of N by GROUP_6:43 ;

hence Ker (nat_hom N) = N by Lm4; :: thesis: verum

for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N

let G be GroupWithOperators of O; :: thesis: for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N

let N be strict normal StableSubgroup of G; :: thesis: Ker (nat_hom N) = N

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;

A1: ( nat_hom N = nat_hom N9 & 1_ (G ./. N) = 1_ (G ./. N9) ) by Def20, Lm34;

the carrier of (Ker (nat_hom N)) = { a where a is Element of G : (nat_hom N) . a = 1_ (G ./. N) } by Def21

.= { a where a is Element of G : (nat_hom N9) . a = 1_ (G ./. N9) } by A1

.= the carrier of (Ker (nat_hom N9)) by GROUP_6:def 9

.= the carrier of N by GROUP_6:43 ;

hence Ker (nat_hom N) = N by Lm4; :: thesis: verum