:: deftheorem Def18 defines OSQuotCharact OSALG_4:def 18 :
for S being locally_directed OrderSortedSign
for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b₅ being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b₅ = OSQuotCharact (R,o) iff for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds
b₅ . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a );