:: deftheorem Def20 defines MSHomQuot MSUALG_4:def 20 :
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 b₅ being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds
( b₅ = MSHomQuot F iff for s being SortSymbol of S holds b₅ . s = MSHomQuot (F,s) );