:: deftheorem Def19 defines MSHomQuot MSUALG_4:def 19 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S st F is_homomorphism U1,U2 holds
for b₆ being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds
( b₆ = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b₆ . (Class ((MSCng (F,s)),x)) = (F . s) . x );