:: deftheorem defines -Image MSAFREE4:def 4 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSAlgebra over S holds
( C is A -Image iff ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ) );