:: deftheorem Def24 defines OSHomQuot OSALG_4:def 24 :
for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2
for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted holds
for b₆ being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) holds
( b₆ = OSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b₆ . (OSClass ((OSCng F),x)) = (F . s) . x );