let S be OrderSortedSign; :: thesis: for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
let U1 be non-empty OSAlgebra of S; :: thesis: for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like
let R be MSEquivalence-like monotone OrderSortedRelation of U1; :: thesis: R is MSCongruence-like
for o being Element of the carrier' 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) by Def28;
hence R is MSCongruence-like by MSUALG_4:def 6; :: thesis: verum