:: deftheorem HOMO defines Homomorphism MSAFREE5:def 13 :
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st ex h being ManySortedFunction of A,B st h is_homomorphism A,B holds
for b₄ being ManySortedFunction of A,B holds
( b₄ is Homomorphism of A,B iff b₄ is_homomorphism A,B );