:: deftheorem Def20 defines nat_hom GROUP_9:def 20 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b₄ being Homomorphism of G,(G ./. N) holds
( b₄ = nat_hom N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b₄ = nat_hom H );