let R be MSEquivalence-like ManySortedRelation of A; :: thesis:
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:
let o be OperSymbol of S; :: according to MSUALG_6:def 7 :: thesis:
let a, b be Function; :: thesis:
assume that
A2: ( a in Args o,A & b in Args o,A ) and
A3: 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:
reconsider a' = a as Element of Args o,A by A2;
A4: dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
defpred S₁[ set , set , set ] means ex c being Element of Args o,A st
( c = A & c₃ = c +* S,(b . S) );
A5: for n being Element of 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 Element of NAT ; :: thesis:
assume ( 1 <= n & n < (len (the_arity_of o)) + 1 ) ; :: thesis:
then ( 1 <= n & n <= len (the_arity_of o) ) by NAT_1:13;
then A6: n in dom (the_arity_of o) by FINSEQ_3:27;
let x be Element of Args o,A; :: thesis:
b . n in the Sorts of A . ((the_arity_of o) /. n) by A2, A6, 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:

end;

consider p being FinSequence of Args o,A such that
A7: len p = (len (the_arity_of o)) + 1 and
A8: ( p . 1 = a' or (len (the_arity_of o)) + 1 = 0 ) and
A9: for i being Element of NAT st 1 <= i & i < (len (the_arity_of o)) + 1 holds
S₁[i,p . i,p . (i + 1)] from RECDEF_1:sch 4(A5);
defpred S₂[ Element of 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 ) ) );
A10: S₂[ 0 ]

proof

assume 0 <= len (the_arity_of o) ; :: thesis:
take a' ; :: thesis:
thus ( a' = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds
a' . j = a . j ) & ( for j being Nat st j in Seg 0 holds
a' . j = b . j ) ) by A8; :: thesis:

end;

A11: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let i be Element of NAT ; :: thesis:
assume that
A12: ( 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
A13: i + 1 <= len (the_arity_of o) ; :: thesis:
A14: i + 1 < (len (the_arity_of o)) + 1 by A13, NAT_1:13;
i <= i + 1 by NAT_1:11;
then consider ci being Element of Args o,A such that
A15: ci = p . (i + 1) and
A16: for j being Element of NAT st j in dom (the_arity_of o) & j > i holds
ci . j = a . j and
A17: for j being Nat st j in Seg i holds
ci . j = b . j by A12, A13, XXREAL_0:2;
A18: i + 1 >= 1 by NAT_1:11;
then consider c being Element of Args o,A such that
A19: ( c = p . (i + 1) & p . ((i + 1) + 1) = c +* (i + 1),(b . (i + 1)) ) by A9, A14;
i + 1 in dom (the_arity_of o) by A13, A18, FINSEQ_3:27;
then b . (i + 1) in the Sorts of A . ((the_arity_of o) /. (i + 1)) by A2, Th2;
then reconsider d = p . ((i + 1) + 1) as Element of Args o,A by A19, Th7;
take d ; :: thesis:
thus d = p . ((i + 1) + 1) ; :: thesis:

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume A20: ( j in dom (the_arity_of o) & j > i + 1 ) ; :: thesis:
then j > i by NAT_1:13;
then ci . j = a . j by A16, A20;
hence d . j = a . j by A15, A19, A20, FUNCT_7:34; :: thesis:

end;

let j be Nat; :: thesis:
assume A21: j in Seg (i + 1) ; :: thesis:
then j in (Seg i) \/ {(i + 1)} by FINSEQ_1:11;
then A22: ( j in Seg i or j in {(i + 1)} ) by XBOOLE_0:def 3;
Seg (i + 1) c= dom (the_arity_of o) by A4, A13, FINSEQ_1:7;
then A23: Seg (i + 1) c= dom c by MSUALG_3:6;

per cases ;

suppose j = i + 1 ; :: thesis:

hence d . j = b . j by A19, A21, A23, FUNCT_7:33; :: thesis:

end;

suppose A24: j <> i + 1 ; :: thesis:

then d . j = c . j by A19, FUNCT_7:34;
hence d . j = b . j by A15, A17, A19, A22, A24, TARSKI:def 1; :: thesis:

end;

A25: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A10, A11);
defpred S₃[ Element of NAT ] means ( S in dom p implies [((Den o,A) . a'),((Den o,A) . (p . S))] in R . (the_result_sort_of o) );
A26: S₃[ 0 ] by FINSEQ_3:27;
A27: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let i be Element of NAT ; :: thesis:
assume that
A28: ( i in dom p implies [((Den o,A) . a'),((Den o,A) . (p . i))] in R . (the_result_sort_of o) ) and
A29: i + 1 in dom p ; :: thesis:
A30: ( Result o,A = the Sorts of A . (the_result_sort_of o) & R . (the_result_sort_of o) is Equivalence_Relation of (the Sorts of A . (the_result_sort_of o)) ) by PRALG_2:10;
A31: ( i <= i + 1 & i + 1 <= len p ) by A29, FINSEQ_3:27, NAT_1:11;
then A32: i <= len p by XXREAL_0:2;

per cases ;

suppose i = 0 ; :: thesis:

hence [((Den o,A) . a'),((Den o,A) . (p . (i + 1)))] in R . (the_result_sort_of o) by A8, A30, EQREL_1:11; :: thesis:

end;

suppose i > 0 ; :: thesis:

then A33: i >= 0 + 1 by NAT_1:13;
A34: i <= len (the_arity_of o) by A7, A31, XREAL_1:8;
i < (len (the_arity_of o)) + 1 by A7, A31, NAT_1:13;
then consider c being Element of Args o,A such that
A35: ( c = p . i & p . (i + 1) = c +* i,(b . i) ) by A9, A33;
A36: i in dom (the_arity_of o) by A33, A34, FINSEQ_3:27;
then reconsider bi = b . i, ci = c . i as Element of A,((the_arity_of o) /. i) by A2, Th2;
reconsider d = c +* i,bi as Element of Args o,A by Th7;
A37: (Den o,A) . d = (transl o,i,c,A) . bi by Def4;
c = c +* i,ci by FUNCT_7:37;
then A38: (Den o,A) . c = (transl o,i,c,A) . ci by Def4;
consider j being Nat such that
A39: i = 1 + j by A33, NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j <= i by A39, NAT_1:11;
then j <= len (the_arity_of o) by A34, XXREAL_0:2;
then A40: 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 A25;
j < i by A39, NAT_1:13;
then c . i = a . i by A35, A36, A39, A40;
then A41: [ci,bi] in R . ((the_arity_of o) /. i) by A3, A36;
transl o,i,c,A is_e.translation_of A,(the_arity_of o) /. i, the_result_sort_of o by A36, Def5;
then [((Den o,A) . c),((Den o,A) . d)] in R . (the_result_sort_of o) by A1, A37, A38, A41;
hence [((Den o,A) . a'),((Den o,A) . (p . (i + 1)))] in R . (the_result_sort_of o) by A28, A32, A33, A35, EQREL_1:13, FINSEQ_3:27; :: thesis:

end;

A42: for i being Element of NAT holds S₃[i] from NAT_1:sch 1(A26, A27);
consider c being Element of Args o,A such that
A43: 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
A44: for j being Nat st j in Seg (len (the_arity_of o)) holds
c . j = b . j by A25;
A45: ( dom c = dom (the_arity_of o) & dom b = dom (the_arity_of o) & dom (the_arity_of o) = Seg (len (the_arity_of o)) ) by A2, FINSEQ_1:def 3, MSUALG_3:6;
then ( b is FinSequence & c is FinSequence ) by FINSEQ_1:def 2;
then A46: c = b by A44, A45, FINSEQ_1:17;
(len (the_arity_of o)) + 1 >= 1 by NAT_1:11;
then (len (the_arity_of o)) + 1 in dom p by A7, FINSEQ_3:27;
hence [((Den o,A) . a),((Den o,A) . b)] in R . (the_result_sort_of o) by A42, A43, A46; :: thesis: