:: deftheorem Def6 defines Image ALG_1:def 6 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
for b₄ being strict SubAlgebra of U2 holds
( b₄ = Image f iff the carrier of b₄ = f .: the carrier of U1 );