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 Def26;
hence R is MSCongruence-like by MSUALG_4:def 4; :: thesis: verum