:: deftheorem defines Image RING_EMB:def 7 :
for G, H being AbGroup
for f being Homomorphism of G,H
for b₄ being strict addLoopStr holds
( b₄ = Image f iff ( the carrier of b₄ = rng f & the addF of b₄ = the addF of H || (rng f) & the ZeroF of b₄ = 0. H ) );