:: deftheorem Def12 defines QuotCharact MSUALG_4:def 12 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b₅ being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b₅ = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b₅ . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a );