let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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 :: thesis: for o being OperSymbol of S
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 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 :: thesis: 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)
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; :: thesis: verum
end;
hence R is MSCongruence of A by MSUALG_4:def 4; :: 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) and
A5: y in Args (o,A) and
A6: 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, A5;
now :: thesis: for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n)
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 A6; :: thesis: verum
end;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) by A3, MSUALG_4:def 4; :: thesis: verum