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