:: deftheorem defines OSQuotArgs OSALG_4:def 15 :
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 Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) holds
( b₅ = OSQuotArgs (R,o) iff for x being Element of Args (o,A) holds b₅ . x = R #_os x );