let R be MSEquivalence-like ManySortedRelation of A; :: thesis: ( R is compatible implies R is invariant )
assume A47: 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 A48: the_result_sort_of o = s2 and
A49: 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
A50: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) and
A51: ( a in Args o,A & f = transl o,i,a,A ) by A49;
let x, y be set ; :: thesis: ( [x,y] in R . s1 implies [(f . x),(f . y)] in R . s2 )
assume A52: [x,y] in R . s1 ; :: thesis: [(f . x),(f . y)] in R . s2
then A53: ( x in the Sorts of A . s1 & y in the Sorts of A . s1 ) by ZFMISC_1:106;
then reconsider ax = a +* i,x, ay = a +* i,y as Element of Args o,A by A50, A51, Th7;
A54: ( dom a = dom (the_arity_of o) & dom ax = dom (the_arity_of o) & dom ay = dom (the_arity_of o) ) by A51, MSUALG_3:6;
A55: ( f . x = (Den o,A) . ax & f . y = (Den o,A) . ay ) by A50, A51, A53, Def4;

now

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) )
assume A56: n in dom (the_arity_of o) ; :: thesis: [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n)
A57: dom (the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 4;
(the_arity_of o) /. n = (the_arity_of o) . n by A56, PARTFUN1:def 8;
then the Sorts of A . ((the_arity_of o) /. n) = (the Sorts of A * (the_arity_of o)) . n by A56, FUNCT_1:23;
then A58: a . n in the Sorts of A . ((the_arity_of o) /. n) by A51, A56, A57, MSUALG_3:6;
( n = i or n <> i ) ;
then ( ( ax . n = x & ay . n = y & n = i ) or ( ax . n = a . n & ay . n = a . n ) ) by A54, A56, FUNCT_7:33, FUNCT_7:34;
hence [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) by A50, A52, A58, EQREL_1:11; :: thesis: verum

end;

hence [(f . x),(f . y)] in R . s2 by A47, A48, A55; :: thesis: verum