:: deftheorem Def13 defines #_os OSALG_4:def 13 :
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 x being Element of Args (o,A)
for b₆ being Element of product ((OSClass R) * (the_arity_of o)) holds
( b₆ = R #_os x iff for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & b₆ . n = OSClass (R,y) ) );