:: deftheorem Def16 defines MSNat_Hom MSUALG_4:def 16 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b₄ being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds
( b₄ = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b₄ . s = MSNat_Hom (U1,R,s) );