:: deftheorem defim defines Image RING_2:def 6 :
for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for b₄ being strict doubleLoopStr holds
( b₄ = Image f iff ( the carrier of b₄ = rng f & the addF of b₄ = the addF of S || (rng f) & the multF of b₄ = the multF of S || (rng f) & the OneF of b₄ = 1. S & the ZeroF of b₄ = 0. S ) );