:: deftheorem Def19 defines OSQuotCharact OSALG_4:def 19 :
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b₄ being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S holds
( b₄ = OSQuotCharact R iff for o being OperSymbol of S holds b₄ . o = OSQuotCharact (R,o) );