:: deftheorem Def5 defines -Image MSAFREE4:def 5 :
for S being non empty non void ManySortedSign
for A, C being non-empty MSAlgebra over S holds
( C is A -Image iff ex h being ManySortedFunction of A,C st h is_epimorphism A,C );