:: deftheorem defines OSQuotRes OSALG_4:def 16 :
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 the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds
( b₄ = OSQuotRes R iff for o being OperSymbol of S holds b₄ . o = OSQuotRes (R,o) );