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 ( (nat_hom N) . a = 1_ (G ./. N) & (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def9, Th29, Th50;
hence a in N by GROUP_2:136; :: thesis: verum

end;

assume a in N ; :: thesis: a in Ker (nat_hom N)
then ( a * N = carr N & (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def9, Th29, GROUP_2:136;
hence a in Ker (nat_hom N) by Th50; :: thesis: verum