:: deftheorem Def8 defines nat_hom GROUP_6:def 8 :
for G being Group
for N being normal Subgroup of G
for b₃ being Function of G,(G ./. N) holds
( b₃ = nat_hom N iff for a being Element of G holds b₃ . a = a * N );