:: deftheorem Def21 defines OSNat_Hom OSALG_4:def 21 :
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for s being Element of S
for b₅ being Function of ( the Sorts of U1 . s),(OSClass (R,s)) holds
( b₅ = OSNat_Hom (U1,R,s) iff for x being Element of the Sorts of U1 . s holds b₅ . x = OSClass (R,x) );