:: deftheorem Def15 defines MSNat_Hom MSUALG_4:def 15 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for s being SortSymbol of S
for b₅ being Function of ( the Sorts of U1 . s),((Class R) . s) holds
( b₅ = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds
b₅ . x = Class ((R . s),x) );