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