let R be MSEquivalence-like ManySortedRelation of A; :: thesis: ( R is compatible implies R is invariant )
assume A52: for o being OperSymbol of S
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) ; :: according to MSUALG_6:def 7 :: thesis: R is invariant
let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def 8 :: thesis: for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
let f be Function; :: thesis: ( f is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
given o being OperSymbol of S such that A53: the_result_sort_of o = s2 and
A54: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,A) & f = transl (o,i,a,A) ) ) ; :: according to MSUALG_6:def 5 :: thesis: for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2
consider i being Element of NAT , a being Function such that
i in dom (the_arity_of o) and
A55: (the_arity_of o) /. i = s1 and
A56: a in Args (o,A) and
A57: f = transl (o,i,a,A) by A54;
let x, y be set ; :: thesis: ( [x,y] in R . s1 implies [(f . x),(f . y)] in R . s2 )
assume A58: [x,y] in R . s1 ; :: thesis: [(f . x),(f . y)] in R . s2
then A59: y in the Sorts of A . s1 by ZFMISC_1:87;
A60: x in the Sorts of A . s1 by A58, ZFMISC_1:87;
then reconsider ax = a +* (i,x), ay = a +* (i,y) as Element of Args (o,A) by A55, A56, A59, Th7;
A61: f . y = (Den (o,A)) . ay by A55, A57, A59, Def4;
A62: dom a = dom (the_arity_of o) by A56, MSUALG_3:6;

A63: now :: thesis: for n being Element of NAT st n in dom (the_arity_of o) holds
[(ax . n),(ay . n)] in R . ((the_arity_of o) /. n)

let n be Element of NAT ; :: thesis: ( n in dom (the_arity_of o) implies [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) )
A64: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
assume A65: n in dom (the_arity_of o) ; :: thesis: [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n)
then (the_arity_of o) /. n = (the_arity_of o) . n by PARTFUN1:def 6;
then A66: the Sorts of A . ((the_arity_of o) /. n) = ( the Sorts of A * (the_arity_of o)) . n by A65, FUNCT_1:13;
( n = i or n <> i ) ;
then ( ( ax . n = x & ay . n = y & n = i ) or ( ax . n = a . n & ay . n = a . n ) ) by A62, A65, FUNCT_7:31, FUNCT_7:32;
hence [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) by A55, A58, A65, A64, A66, EQREL_1:5, MSUALG_3:6; :: thesis: verum

end;

f . x = (Den (o,A)) . ax by A55, A57, A60, Def4;
hence [(f . x),(f . y)] in R . s2 by A52, A53, A61, A63; :: thesis: verum