:: deftheorem Def25 defines OSHomQuot OSALG_4:def 25 :
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for b₅ being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 holds
( b₅ = OSHomQuot F iff for s being Element of S holds b₅ . s = OSHomQuot (F,s) );