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