let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being MSEquivalence-like ManySortedRelation of A holds
( R is compatible iff R is MSCongruence of A )
let A be non-empty MSAlgebra of S; :: thesis: for R being MSEquivalence-like ManySortedRelation of A holds
( R is compatible iff R is MSCongruence of A )
let R be MSEquivalence-like ManySortedRelation of A; :: thesis: ( R is compatible iff R is MSCongruence of A )

hereby :: thesis: ( R is MSCongruence of A implies R is compatible )

assume A1: R is compatible ; :: thesis: R is MSCongruence of A

now

let o be OperSymbol of S; :: thesis: for x, y being Element of Args o,A 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,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o)
let x, y be Element of Args o,A; :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o) )
assume A2: for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o)

now

let n be Element of NAT ; :: thesis: ( n in dom (the_arity_of o) implies [(x . n),(y . n)] in R . ((the_arity_of o) /. n) )
assume n in dom (the_arity_of o) ; :: thesis: [(x . n),(y . n)] in R . ((the_arity_of o) /. n)
then n in dom x by MSUALG_3:6;
hence [(x . n),(y . n)] in R . ((the_arity_of o) /. n) by A2; :: thesis: verum

end;

hence [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o) by A1, Def7; :: thesis: verum

end;

hence R is MSCongruence of A by MSUALG_4:def 6; :: thesis: verum

end;

assume A3: R is MSCongruence of A ; :: thesis: R is compatible
let o be OperSymbol of S; :: according to MSUALG_6:def 7 :: thesis: 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)
let x, y be Function; :: thesis: ( x in Args o,A & y in Args o,A & ( for n being Element of NAT st n in dom (the_arity_of o) holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o) )
assume that
A4: ( x in Args o,A & y in Args o,A ) and
A5: for n being Element of NAT st n in dom (the_arity_of o) holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o)
reconsider x = x, y = y as Element of Args o,A by A4;

now

let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in R . ((the_arity_of o) /. n) )
assume n in dom x ; :: thesis: [(x . n),(y . n)] in R . ((the_arity_of o) /. n)
then n in dom (the_arity_of o) by MSUALG_3:6;
hence [(x . n),(y . n)] in R . ((the_arity_of o) /. n) by A5; :: thesis: verum

end;

hence [((Den o,A) . x),((Den o,A) . y)] in R . (the_result_sort_of o) by A3, MSUALG_4:def 6; :: thesis: verum