let R be MSEquivalence-like ManySortedRelation of A; :: thesis: ( R is invariant implies R is compatible )
assume A1: for s1, s2 being SortSymbol of S
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 ; :: according to MSUALG_6:def 8 :: 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 a, b be Function; :: thesis: ( 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) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) )
assume that
A2: a in Args (o,A) and
A3: b in Args (o,A) and
A4: 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) ; :: thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o)
A5: dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
reconsider a9 = a as Element of Args (o,A) by A2;
defpred S₁[ set , set , set ] means ex c being Element of Args (o,A) st
( c = A & c₃ = c +* (S,(b . S)) );
A6: for n being Nat st 1 <= n & n < (len (the_arity_of o)) + 1 holds
for x being Element of Args (o,A) ex y being Element of Args (o,A) st S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < (len (the_arity_of o)) + 1 implies for x being Element of Args (o,A) ex y being Element of Args (o,A) st S₁[n,x,y] )
assume that
A7: 1 <= n and
A8: n < (len (the_arity_of o)) + 1 ; :: thesis: for x being Element of Args (o,A) ex y being Element of Args (o,A) st S₁[n,x,y]
let x be Element of Args (o,A); :: thesis: ex y being Element of Args (o,A) st S₁[n,x,y]
n <= len (the_arity_of o) by A8, NAT_1:13;
then n in dom (the_arity_of o) by A7, FINSEQ_3:25;
then b . n in the Sorts of A . ((the_arity_of o) /. n) by A3, Th2;
then x +* (n,(b . n)) in Args (o,A) by Th7;
hence ex y being Element of Args (o,A) st S₁[n,x,y] ; :: thesis: verum

end;

consider p being FinSequence of Args (o,A) such that
A9: len p = (len (the_arity_of o)) + 1 and
A10: ( p . 1 = a9 or (len (the_arity_of o)) + 1 = 0 ) and
A11: for i being Nat st 1 <= i & i < (len (the_arity_of o)) + 1 holds
S₁[i,p . i,p . (i + 1)] from RECDEF_1:sch 4(A6);
(len (the_arity_of o)) + 1 >= 1 by NAT_1:11;
then A12: (len (the_arity_of o)) + 1 in dom p by A9, FINSEQ_3:25;
defpred S₂[ Nat] means ( S <= len (the_arity_of o) implies ex c being Element of Args (o,A) st
( c = p . (S + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > S holds
c . j = a . j ) & ( for j being Nat st j in Seg S holds
c . j = b . j ) ) );
A13: dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
A14: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume that
A15: ( i <= len (the_arity_of o) implies ex c being Element of Args (o,A) st
( c = p . (i + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i holds
c . j = a . j ) & ( for j being Nat st j in Seg i holds
c . j = b . j ) ) ) and
A16: i + 1 <= len (the_arity_of o) ; :: thesis: ex c being Element of Args (o,A) st
( c = p . ((i + 1) + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds
c . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds
c . j = b . j ) )
i + 1 < (len (the_arity_of o)) + 1 by A16, NAT_1:13;
then consider c being Element of Args (o,A) such that
A17: c = p . (i + 1) and
A18: p . ((i + 1) + 1) = c +* ((i + 1),(b . (i + 1))) by A11, NAT_1:11;
i + 1 >= 1 by NAT_1:11;
then i + 1 in dom (the_arity_of o) by A16, FINSEQ_3:25;
then b . (i + 1) in the Sorts of A . ((the_arity_of o) /. (i + 1)) by A3, Th2;
then reconsider d = p . ((i + 1) + 1) as Element of Args (o,A) by A18, Th7;
take d ; :: thesis: ( d = p . ((i + 1) + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds
d . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds
d . j = b . j ) )
thus d = p . ((i + 1) + 1) ; :: thesis: ( ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds
d . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds
d . j = b . j ) )
Seg (i + 1) c= dom (the_arity_of o) by A13, A16, FINSEQ_1:5;
then A19: Seg (i + 1) c= dom c by MSUALG_3:6;
i <= i + 1 by NAT_1:11;
then consider ci being Element of Args (o,A) such that
A20: ci = p . (i + 1) and
A21: for j being Element of NAT st j in dom (the_arity_of o) & j > i holds
ci . j = a . j and
A22: for j being Nat st j in Seg i holds
ci . j = b . j by A15, A16, XXREAL_0:2;

hereby :: thesis: for j being Nat st j in Seg (i + 1) holds
d . j = b . j

let j be Element of NAT ; :: thesis: ( j in dom (the_arity_of o) & j > i + 1 implies d . j = a . j )
assume that
A23: j in dom (the_arity_of o) and
A24: j > i + 1 ; :: thesis: d . j = a . j
j > i by A24, NAT_1:13;
then ci . j = a . j by A21, A23;
hence d . j = a . j by A20, A17, A18, A24, FUNCT_7:32; :: thesis: verum

end;

let j be Nat; :: thesis: ( j in Seg (i + 1) implies d . j = b . j )
assume A25: j in Seg (i + 1) ; :: thesis: d . j = b . j
then j in (Seg i) \/ {(i + 1)} by FINSEQ_1:9;
then A26: ( j in Seg i or j in {(i + 1)} ) by XBOOLE_0:def 3;

per cases ( j = i + 1 or j <> i + 1 ) ;

suppose j = i + 1 ; :: thesis: d . j = b . j

hence d . j = b . j by A18, A25, A19, FUNCT_7:31; :: thesis: verum

end;

suppose A27: j <> i + 1 ; :: thesis: d . j = b . j

then d . j = c . j by A18, FUNCT_7:32;
hence d . j = b . j by A20, A22, A17, A26, A27, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A28: S₂[ 0 ]

proof

assume 0 <= len (the_arity_of o) ; :: thesis: ex c being Element of Args (o,A) st
( c = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds
c . j = a . j ) & ( for j being Nat st j in Seg 0 holds
c . j = b . j ) )
take a9 ; :: thesis: ( a9 = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds
a9 . j = a . j ) & ( for j being Nat st j in Seg 0 holds
a9 . j = b . j ) )
thus ( a9 = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds
a9 . j = a . j ) & ( for j being Nat st j in Seg 0 holds
a9 . j = b . j ) ) by A10; :: thesis: verum

end;

A29: for i being Nat holds S₂[i] from NAT_1:sch 2(A28, A14);
then consider c being Element of Args (o,A) such that
A30: c = p . ((len (the_arity_of o)) + 1) and
for j being Element of NAT st j in dom (the_arity_of o) & j > len (the_arity_of o) holds
c . j = a . j and
A31: for j being Nat st j in Seg (len (the_arity_of o)) holds
c . j = b . j ;
defpred S₃[ Nat] means ( S in dom p implies [((Den (o,A)) . a9),((Den (o,A)) . (p . S))] in R . (the_result_sort_of o) );
A32: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

A33: Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3;
let i be Nat; :: thesis: ( S₃[i] implies S₃[i + 1] )
assume that
A34: ( i in dom p implies [((Den (o,A)) . a9),((Den (o,A)) . (p . i))] in R . (the_result_sort_of o) ) and
A35: i + 1 in dom p ; :: thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o)
A36: i + 1 <= len p by A35, FINSEQ_3:25;
i <= i + 1 by NAT_1:11;
then A37: i <= len p by A36, XXREAL_0:2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o)

hence [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) by A10, A33, EQREL_1:5; :: thesis: verum

end;

suppose i > 0 ; :: thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o)

then A38: i >= 0 + 1 by NAT_1:13;
then consider j being Nat such that
A39: i = 1 + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
i < (len (the_arity_of o)) + 1 by A9, A36, NAT_1:13;
then consider c being Element of Args (o,A) such that
A40: c = p . i and
A41: p . (i + 1) = c +* (i,(b . i)) by A11, A38;
A42: i <= len (the_arity_of o) by A9, A36, XREAL_1:6;
then A43: i in dom (the_arity_of o) by A38, FINSEQ_3:25;
then reconsider bi = b . i, ci = c . i as Element of A,((the_arity_of o) /. i) by A3, Th2;
j <= i by A39, NAT_1:11;
then A44: ex c being Element of Args (o,A) st
( c = p . (j + 1) & ( for k being Element of NAT st k in dom (the_arity_of o) & k > j holds
c . k = a . k ) & ( for k being Nat st k in Seg j holds
c . k = b . k ) ) by A29, A42, XXREAL_0:2;
j < i by A39, NAT_1:13;
then c . i = a . i by A40, A43, A39, A44;
then A45: [ci,bi] in R . ((the_arity_of o) /. i) by A4, A43;
reconsider d = c +* (i,bi) as Element of Args (o,A) by Th7;
A46: (Den (o,A)) . d = (transl (o,i,c,A)) . bi by Def4;
c = c +* (i,ci) by FUNCT_7:35;
then A47: (Den (o,A)) . c = (transl (o,i,c,A)) . ci by Def4;
transl (o,i,c,A) is_e.translation_of A,(the_arity_of o) /. i, the_result_sort_of o by A43;
then [((Den (o,A)) . c),((Den (o,A)) . d)] in R . (the_result_sort_of o) by A1, A46, A47, A45;
hence [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) by A34, A37, A38, A40, A41, EQREL_1:7, FINSEQ_3:25; :: thesis: verum

end;

end;

end;

A48: dom b = dom (the_arity_of o) by A3, MSUALG_3:6;
A49: S₃[ 0 ] by FINSEQ_3:25;
A50: for i being Nat holds S₃[i] from NAT_1:sch 2(A49, A32);
A51: dom c = dom (the_arity_of o) by MSUALG_3:6;
c = b by A31, A51, A48, A5;
hence [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) by A50, A30, A12; :: thesis: verum