:: deftheorem Def12 defines Image MSUALG_3:def 12 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b₅ being strict non-empty MSSubAlgebra of U2 holds
( b₅ = Image F iff the Sorts of b₅ = F .:.: the Sorts of U1 );