:: deftheorem Def4 defines MSCongruence-like MSUALG_4:def 4 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1 holds
( R is MSCongruence-like iff for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in R . (the_result_sort_of o) );