let R be MSEquivalence-like ManySortedRelation of A; ( 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)
; MSUALG_6:def 7 R is invariant
let s1, s2 be SortSymbol of S; MSUALG_6:def 8 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; ( 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) ) )
; MSUALG_6:def 5 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 ; ( [x,y] in R . s1 implies [(f . x),(f . y)] in R . s2 )
assume A58:
[x,y] in R . s1
; [(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 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 ;
( 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)
;
[(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;
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; verum