:: deftheorem Def22 defines OSNat_Hom OSALG_4:def 22 :
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for b₄ being ManySortedFunction of U1,(QuotOSAlg (U1,R)) holds
( b₄ = OSNat_Hom (U1,R) iff for s being Element of S holds b₄ . s = OSNat_Hom (U1,R,s) );