:: deftheorem Def14 defines OSQuotRes OSALG_4:def 14 :
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 (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) holds
( b₅ = OSQuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b₅ . x = OSClass (R,x) );