:: deftheorem Def13 defines QuotCharact MSUALG_4:def 13 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b₄ being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds
( b₄ = QuotCharact R iff for o being OperSymbol of S holds b₄ . o = QuotCharact (R,o) );