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 Lm7;
A1: ( nat_hom N = nat_hom N9 & 1_ (G ./. N) = 1_ (G ./. N9) ) by Def23, Lm35;
the carrier of (Ker (nat_hom N)) = { a where a is Element of G : (nat_hom N) . a = 1_ (G ./. N) } by Def24
.= { 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 10
.= the carrier of N by GROUP_6:52 ;
hence Ker (nat_hom N) = N by Lm5; :: thesis: verum