let G be Group; :: thesis: for N being strict normal Subgroup of G holds Ker (nat_hom N) = N
let N be strict normal Subgroup of G; :: thesis: Ker (nat_hom N) = N
let a be Element of G; :: according to GROUP_2:def 6 :: thesis: ( ( not a in Ker (nat_hom N) or a in N ) & ( not a in N or a in Ker (nat_hom N) ) )
thus ( a in Ker (nat_hom N) implies a in N ) :: thesis: ( not a in N or a in Ker (nat_hom N) )

proof

assume a in Ker (nat_hom N) ; :: thesis: a in N
then A1: (nat_hom N) . a = 1_ (G ./. N) by Th41;
( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24;
hence a in N by A1, GROUP_2:113; :: thesis: verum

end;

assume a in N ; :: thesis: a in Ker (nat_hom N)
then A2: a * N = carr N by GROUP_2:113;
( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24;
hence a in Ker (nat_hom N) by A2, Th41; :: thesis: verum