:: deftheorem defines compatible MSUALG_6:def 7 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for R being ManySortedRelation of A holds
( R is compatible iff for o being OperSymbol of S
for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) );