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' by Def23;
A2: 1_ (G ./. N) = 1_ (G ./. N') by 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 N') . a = 1_ (G ./. N') } by A1, A2
.= 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