let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for o being OperSymbol of S

for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let A be non-empty MSAlgebra over S; :: thesis: for o being OperSymbol of S

for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let o be OperSymbol of S; :: thesis: for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let C1, C2 be MSCongruence of A; :: thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let C be MSEquivalence-like ManySortedRelation of A; :: thesis: ( C = C1 "\/" C2 implies for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume A1: C = C1 "\/" C2 ; :: thesis: for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

consider C9 being ManySortedRelation of the Sorts of A such that

A2: C9 = C1 (\/) C2 and

A3: C1 "\/" C2 = EqCl C9 by Def4;

A4: (C1 . (the_result_sort_of o)) "\/" (C2 . (the_result_sort_of o)) = EqCl ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) by Th1

.= EqCl (C9 . (the_result_sort_of o)) by A2, PBOOLE:def 4

.= (C1 "\/" C2) . (the_result_sort_of o) by A3, Def3 ;

consider D9 being ManySortedRelation of the Sorts of A such that

A5: D9 = C1 (\/) C2 and

A6: C1 "\/" C2 = EqCl D9 by Def4;

let x1, y1 be object ; :: thesis: for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let n be Element of NAT ; :: thesis: for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let a1, a2, b1 be FinSequence; :: thesis: ( len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) implies for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume that

A7: len a1 = n and

A8: len a1 = len a2 and

A9: for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ; :: thesis: ( not [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) or not [x1,y1] in C . ((the_arity_of o) /. (n + 1)) or for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

A10: (C1 . ((the_arity_of o) /. (n + 1))) "\/" (C2 . ((the_arity_of o) /. (n + 1))) = EqCl ((C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))) by Th1

.= EqCl (D9 . ((the_arity_of o) /. (n + 1))) by A5, PBOOLE:def 4

.= (C1 "\/" C2) . ((the_arity_of o) /. (n + 1)) by A6, Def3 ;

set y = (a2 ^ <*y1*>) ^ b1;

assume that

A11: [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) and

A12: [x1,y1] in C . ((the_arity_of o) /. (n + 1)) ; :: thesis: for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let x be Element of Args (o,A); :: thesis: ( x = (a1 ^ <*x1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume A13: x = (a1 ^ <*x1*>) ^ b1 ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

A14: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def 2

.= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15

.= Result (o,A) by MSUALG_1:def 5 ;

then (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ;

then consider p being FinSequence such that

A15: 1 <= len p and

A16: (Den (o,A)) . ((a1 ^ <*x1*>) ^ b1) = p . 1 and

A17: (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) and

A18: for i being Nat st 1 <= i & i < len p holds

[(p . i),(p . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A1, A11, A13, A4, EQREL_1:28;

x1 in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A12, ZFMISC_1:87;

then consider f being FinSequence such that

A19: 1 <= len f and

A20: x1 = f . 1 and

A21: y1 = f . (len f) and

A22: for i being Nat st 1 <= i & i < len f holds

[(f . i),(f . (i + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A1, A12, A10, EQREL_1:28;

deffunc H_{1}( Nat) -> set = (Den (o,A)) . ((a2 ^ <*(f . $1)*>) ^ b1);

consider g being FinSequence such that

A23: ( len g = len f & ( for i being Nat st i in dom g holds

g . i = H_{1}(i) ) )
from FINSEQ_1:sch 2();

A24: dom g = Seg (len f) by A23, FINSEQ_1:def 3;

A25: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg (len (a1 ^ (<*x1*> ^ b1))) by FINSEQ_1:32

.= Seg ((len a2) + (len (<*x1*> ^ b1))) by A8, FINSEQ_1:22

.= Seg (len (a2 ^ (<*x1*> ^ b1))) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:32

.= dom ((a2 ^ <*x1*>) ^ b1) by FINSEQ_1:def 3 ;

ex q being FinSequence st

( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

for o being OperSymbol of S

for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let A be non-empty MSAlgebra over S; :: thesis: for o being OperSymbol of S

for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let o be OperSymbol of S; :: thesis: for C1, C2 being MSCongruence of A

for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let C1, C2 be MSCongruence of A; :: thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds

for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let C be MSEquivalence-like ManySortedRelation of A; :: thesis: ( C = C1 "\/" C2 implies for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume A1: C = C1 "\/" C2 ; :: thesis: for x1, y1 being object

for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

consider C9 being ManySortedRelation of the Sorts of A such that

A2: C9 = C1 (\/) C2 and

A3: C1 "\/" C2 = EqCl C9 by Def4;

A4: (C1 . (the_result_sort_of o)) "\/" (C2 . (the_result_sort_of o)) = EqCl ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) by Th1

.= EqCl (C9 . (the_result_sort_of o)) by A2, PBOOLE:def 4

.= (C1 "\/" C2) . (the_result_sort_of o) by A3, Def3 ;

consider D9 being ManySortedRelation of the Sorts of A such that

A5: D9 = C1 (\/) C2 and

A6: C1 "\/" C2 = EqCl D9 by Def4;

let x1, y1 be object ; :: thesis: for n being Element of NAT

for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let n be Element of NAT ; :: thesis: for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds

for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let a1, a2, b1 be FinSequence; :: thesis: ( len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) implies for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume that

A7: len a1 = n and

A8: len a1 = len a2 and

A9: for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ; :: thesis: ( not [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) or not [x1,y1] in C . ((the_arity_of o) /. (n + 1)) or for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

A10: (C1 . ((the_arity_of o) /. (n + 1))) "\/" (C2 . ((the_arity_of o) /. (n + 1))) = EqCl ((C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))) by Th1

.= EqCl (D9 . ((the_arity_of o) /. (n + 1))) by A5, PBOOLE:def 4

.= (C1 "\/" C2) . ((the_arity_of o) /. (n + 1)) by A6, Def3 ;

set y = (a2 ^ <*y1*>) ^ b1;

assume that

A11: [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) and

A12: [x1,y1] in C . ((the_arity_of o) /. (n + 1)) ; :: thesis: for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds

[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

let x be Element of Args (o,A); :: thesis: ( x = (a1 ^ <*x1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )

assume A13: x = (a1 ^ <*x1*>) ^ b1 ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

A14: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def 2

.= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15

.= Result (o,A) by MSUALG_1:def 5 ;

then (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ;

then consider p being FinSequence such that

A15: 1 <= len p and

A16: (Den (o,A)) . ((a1 ^ <*x1*>) ^ b1) = p . 1 and

A17: (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) and

A18: for i being Nat st 1 <= i & i < len p holds

[(p . i),(p . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A1, A11, A13, A4, EQREL_1:28;

x1 in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A12, ZFMISC_1:87;

then consider f being FinSequence such that

A19: 1 <= len f and

A20: x1 = f . 1 and

A21: y1 = f . (len f) and

A22: for i being Nat st 1 <= i & i < len f holds

[(f . i),(f . (i + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A1, A12, A10, EQREL_1:28;

deffunc H

consider g being FinSequence such that

A23: ( len g = len f & ( for i being Nat st i in dom g holds

g . i = H

A24: dom g = Seg (len f) by A23, FINSEQ_1:def 3;

A25: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg (len (a1 ^ (<*x1*> ^ b1))) by FINSEQ_1:32

.= Seg ((len a2) + (len (<*x1*> ^ b1))) by A8, FINSEQ_1:22

.= Seg (len (a2 ^ (<*x1*> ^ b1))) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:32

.= dom ((a2 ^ <*x1*>) ^ b1) by FINSEQ_1:def 3 ;

ex q being FinSequence st

( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

proof

hence
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
by A1, A4, A14, EQREL_1:28; :: thesis: verum
take q = p ^ g; :: thesis: ( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

A26: len q = (len p) + (len g) by FINSEQ_1:22;

hence 1 <= len q by A15, NAT_1:12; :: thesis: ( (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

1 in dom p by A15, FINSEQ_3:25;

hence q . 1 = (Den (o,A)) . x by A13, A16, FINSEQ_1:def 7; :: thesis: ( (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

A27: len g in Seg (len f) by A19, A23, FINSEQ_1:1;

then len g in dom g by A23, FINSEQ_1:def 3;

hence q . (len q) = g . (len g) by A26, FINSEQ_1:def 7

.= (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) by A21, A23, A24, A27 ;

:: thesis: for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

A28: len p <> 0 by A15;

end;[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

A26: len q = (len p) + (len g) by FINSEQ_1:22;

hence 1 <= len q by A15, NAT_1:12; :: thesis: ( (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

1 in dom p by A15, FINSEQ_3:25;

hence q . 1 = (Den (o,A)) . x by A13, A16, FINSEQ_1:def 7; :: thesis: ( (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )

A27: len g in Seg (len f) by A19, A23, FINSEQ_1:1;

then len g in dom g by A23, FINSEQ_1:def 3;

hence q . (len q) = g . (len g) by A26, FINSEQ_1:def 7

.= (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) by A21, A23, A24, A27 ;

:: thesis: for i being Nat st 1 <= i & i < len q holds

[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

A28: len p <> 0 by A15;

hereby :: thesis: verum

let i be Nat; :: thesis: ( 1 <= i & i < len q implies [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )

assume that

A29: 1 <= i and

A30: i < len q ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

A31: ( ( 1 <= i & i < len p ) or ( (len p) + 1 <= i & i < len q ) or i = len p )

.= dom (the_arity_of o) by MSUALG_3:6

.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;

A35: len ((a2 ^ <*x1*>) ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32

.= (len a2) + (len (<*x1*> ^ b1)) by FINSEQ_1:22

.= len (a1 ^ (<*x1*> ^ b1)) by A8, FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:32

.= len (the_arity_of o) by A34, FINSEQ_1:6 ;

end;assume that

A29: 1 <= i and

A30: i < len q ; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

A31: ( ( 1 <= i & i < len p ) or ( (len p) + 1 <= i & i < len q ) or i = len p )

proof

A34: Seg (len ((a1 ^ <*x1*>) ^ b1)) =
dom x
by A13, FINSEQ_1:def 3
assume that

A32: ( not 1 <= i or not i < len p ) and

A33: ( not (len p) + 1 <= i or not i < len q ) ; :: thesis: i = len p

i <= len p by A30, A33, NAT_1:13;

hence i = len p by A29, A32, XXREAL_0:1; :: thesis: verum

end;A32: ( not 1 <= i or not i < len p ) and

A33: ( not (len p) + 1 <= i or not i < len q ) ; :: thesis: i = len p

i <= len p by A30, A33, NAT_1:13;

hence i = len p by A29, A32, XXREAL_0:1; :: thesis: verum

.= dom (the_arity_of o) by MSUALG_3:6

.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;

A35: len ((a2 ^ <*x1*>) ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32

.= (len a2) + (len (<*x1*> ^ b1)) by FINSEQ_1:22

.= len (a1 ^ (<*x1*> ^ b1)) by A8, FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:32

.= len (the_arity_of o) by A34, FINSEQ_1:6 ;

A36: now :: thesis: for k being Element of NAT st k in dom x holds

x . k in the Sorts of A . ((the_arity_of o) /. k)

A41:
ex i1 being Nat st len p = i1 + 1
by A28, NAT_1:6;x . k in the Sorts of A . ((the_arity_of o) /. k)

let k be Element of NAT ; :: thesis: ( k in dom x implies x . k in the Sorts of A . ((the_arity_of o) /. k) )

assume k in dom x ; :: thesis: x . k in the Sorts of A . ((the_arity_of o) /. k)

then A37: k in Seg (len (the_arity_of o)) by A25, A35, FINSEQ_1:def 3;

then A38: k in dom (the_arity_of o) by FINSEQ_1:def 3;

then A39: k in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def 2;

reconsider dz = dom (the_arity_of o) as non empty set by A37, FINSEQ_1:def 3;

reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ;

A40: not product so is empty ;

pi ((Args (o,A)),k) = pi (((( the Sorts of A #) * the Arity of S) . o),k) by MSUALG_1:def 4

.= pi ((( the Sorts of A #) . ( the Arity of S . o)),k) by FUNCT_2:15

.= pi ((( the Sorts of A #) . (the_arity_of o)),k) by MSUALG_1:def 1

.= pi ((product ( the Sorts of A * (the_arity_of o))),k) by FINSEQ_2:def 5

.= ( the Sorts of A * (the_arity_of o)) . k by A39, A40, CARD_3:12

.= the Sorts of A . ((the_arity_of o) . k) by A38, FUNCT_1:13

.= the Sorts of A . ((the_arity_of o) /. k) by A38, PARTFUN1:def 6 ;

hence x . k in the Sorts of A . ((the_arity_of o) /. k) by CARD_3:def 6; :: thesis: verum

end;assume k in dom x ; :: thesis: x . k in the Sorts of A . ((the_arity_of o) /. k)

then A37: k in Seg (len (the_arity_of o)) by A25, A35, FINSEQ_1:def 3;

then A38: k in dom (the_arity_of o) by FINSEQ_1:def 3;

then A39: k in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def 2;

reconsider dz = dom (the_arity_of o) as non empty set by A37, FINSEQ_1:def 3;

reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ;

A40: not product so is empty ;

pi ((Args (o,A)),k) = pi (((( the Sorts of A #) * the Arity of S) . o),k) by MSUALG_1:def 4

.= pi ((( the Sorts of A #) . ( the Arity of S . o)),k) by FUNCT_2:15

.= pi ((( the Sorts of A #) . (the_arity_of o)),k) by MSUALG_1:def 1

.= pi ((product ( the Sorts of A * (the_arity_of o))),k) by FINSEQ_2:def 5

.= ( the Sorts of A * (the_arity_of o)) . k by A39, A40, CARD_3:12

.= the Sorts of A . ((the_arity_of o) . k) by A38, FUNCT_1:13

.= the Sorts of A . ((the_arity_of o) /. k) by A38, PARTFUN1:def 6 ;

hence x . k in the Sorts of A . ((the_arity_of o) /. k) by CARD_3:def 6; :: thesis: verum

now :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))end;

hence
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
; :: thesis: verumper cases
( ( 1 <= i & i < len p ) or i = len p or ( (len p) + 1 <= i & i < len q ) )
by A31;

end;

suppose A42:
( 1 <= i & i < len p )
; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then A43:
i + 1 <= len p
by NAT_1:13;

1 <= i + 1 by A42, NAT_1:13;

then i + 1 in dom p by A43, FINSEQ_3:25;

then A44: q . (i + 1) = p . (i + 1) by FINSEQ_1:def 7;

i in dom p by A42, FINSEQ_3:25;

then q . i = p . i by FINSEQ_1:def 7;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A18, A42, A44; :: thesis: verum

end;1 <= i + 1 by A42, NAT_1:13;

then i + 1 in dom p by A43, FINSEQ_3:25;

then A44: q . (i + 1) = p . (i + 1) by FINSEQ_1:def 7;

i in dom p by A42, FINSEQ_3:25;

then q . i = p . i by FINSEQ_1:def 7;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A18, A42, A44; :: thesis: verum

suppose A45:
i = len p
; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then
i in Seg (len p)
by A41, FINSEQ_1:4;

then i in dom p by FINSEQ_1:def 3;

then A46: q . i = (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A17, A45, FINSEQ_1:def 7;

A47: 1 in Seg (len g) by A19, A23, FINSEQ_1:1;

then 1 in dom g by FINSEQ_1:def 3;

then A48: q . (i + 1) = g . 1 by A45, FINSEQ_1:def 7

.= (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A20, A23, A24, A47 ;

for k being Nat st k in dom ((a2 ^ <*x1*>) ^ b1) holds

((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A55: field (C2 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;

field (C1 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;

then field ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) = ( the Sorts of A . (the_result_sort_of o)) \/ ( the Sorts of A . (the_result_sort_of o)) by A55, RELAT_1:18

.= the Sorts of A . (the_result_sort_of o) ;

then A56: (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def 9;

(Den (o,A)) . de in the Sorts of A . (the_result_sort_of o) by A14;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A46, A48, A56, RELAT_2:def 1; :: thesis: verum

end;then i in dom p by FINSEQ_1:def 3;

then A46: q . i = (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A17, A45, FINSEQ_1:def 7;

A47: 1 in Seg (len g) by A19, A23, FINSEQ_1:1;

then 1 in dom g by FINSEQ_1:def 3;

then A48: q . (i + 1) = g . 1 by A45, FINSEQ_1:def 7

.= (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A20, A23, A24, A47 ;

for k being Nat st k in dom ((a2 ^ <*x1*>) ^ b1) holds

((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

then reconsider de = (a2 ^ <*x1*>) ^ b1 as Element of Args (o,A) by A35, MSAFREE2:5;
let k be Nat; :: thesis: ( k in dom ((a2 ^ <*x1*>) ^ b1) implies ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )

assume A49: k in dom ((a2 ^ <*x1*>) ^ b1) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A50: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32;

end;assume A49: k in dom ((a2 ^ <*x1*>) ^ b1) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A50: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32;

now :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)end;

hence
((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
; :: thesis: verumper cases
( k in dom a2 or ex n1 being Nat st

( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ) by A50, FINSEQ_1:25;

end;

( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ) by A50, FINSEQ_1:25;

suppose A51:
k in dom a2
; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then
k in Seg (len a2)
by FINSEQ_1:def 3;

then k in dom a1 by A8, FINSEQ_1:def 3;

then A52: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A51, FINSEQ_1:def 7 ;

hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A52, ZFMISC_1:87; :: thesis: verum

end;then k in dom a1 by A8, FINSEQ_1:def 3;

then A52: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A51, FINSEQ_1:def 7 ;

hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A52, ZFMISC_1:87; :: thesis: verum

suppose
ex n1 being Nat st

( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ; :: thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n1 being Nat such that

A53: n1 in dom (<*x1*> ^ b1) and

A54: k = (len a2) + n1 ;

((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32

.= (<*x1*> ^ b1) . n1 by A53, A54, FINSEQ_1:def 7

.= (a1 ^ (<*x1*> ^ b1)) . k by A8, A53, A54, FINSEQ_1:def 7

.= x . k by A13, FINSEQ_1:32 ;

hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A25, A36, A49; :: thesis: verum

end;A53: n1 in dom (<*x1*> ^ b1) and

A54: k = (len a2) + n1 ;

((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32

.= (<*x1*> ^ b1) . n1 by A53, A54, FINSEQ_1:def 7

.= (a1 ^ (<*x1*> ^ b1)) . k by A8, A53, A54, FINSEQ_1:def 7

.= x . k by A13, FINSEQ_1:32 ;

hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A25, A36, A49; :: thesis: verum

A55: field (C2 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;

field (C1 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;

then field ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) = ( the Sorts of A . (the_result_sort_of o)) \/ ( the Sorts of A . (the_result_sort_of o)) by A55, RELAT_1:18

.= the Sorts of A . (the_result_sort_of o) ;

then A56: (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def 9;

(Den (o,A)) . de in the Sorts of A . (the_result_sort_of o) by A14;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A46, A48, A56, RELAT_2:def 1; :: thesis: verum

suppose A57:
( (len p) + 1 <= i & i < len q )
; :: thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

then
len p < i
by NAT_1:13;

then reconsider j = i - (len p) as Element of NAT by NAT_1:21;

A58: 1 <= j + 1 by NAT_1:12;

len f = (len q) - (len p) by A23, A26, XCMPLX_1:26;

then A59: j < len f by A57, XREAL_1:9;

then j + 1 <= len f by NAT_1:13;

then j + 1 in Seg (len f) by A58, FINSEQ_1:1;

then A60: (i + 1) - (len p) in Seg (len f) by XCMPLX_1:29;

A61: 1 <= j by A57, XREAL_1:19;

then A62: [(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A59;

then A63: f . ((i - (len p)) + 1) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by ZFMISC_1:87;

A64: for k being Nat st k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) holds

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A78: for k being Nat st k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) holds

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

j <= len f by A23, A26, A57, XREAL_1:19;

then A93: i - (len p) in Seg (len f) by A92, FINSEQ_1:1;

A94: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def 3

.= dom (the_arity_of o) by MSUALG_3:6

.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;

A95: len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + 1) + (len b1) by FINSEQ_1:40

.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40

.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22

.= len (the_arity_of o) by A94, FINSEQ_1:6 ;

len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + 1) + (len b1) by FINSEQ_1:40

.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40

.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22

.= len (the_arity_of o) by A94, FINSEQ_1:6 ;

then reconsider d1 = (a2 ^ <*(f . (i - (len p)))*>) ^ b1, d2 = (a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as Element of Args (o,A) by A78, A64, A95, MSAFREE2:5;

A96: q . i = g . (i - (len p)) by A26, A57, FINSEQ_1:23

.= (Den (o,A)) . d1 by A23, A24, A93 ;

(i + 1) - (len p) = (i - (len p)) + 1 by XCMPLX_1:29;

then A97: [(f . (i - (len p))),(f . ((i + 1) - (len p)))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A61, A59;

A98: i + 1 <= len q by A57, NAT_1:13;

(len p) + 1 <= i + 1 by A57, NAT_1:12;

then q . (i + 1) = g . ((i + 1) - (len p)) by A26, A98, FINSEQ_1:23

.= (Den (o,A)) . d2 by A23, A24, A60 ;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A7, A8, A96, A97, Th12; :: thesis: verum

end;then reconsider j = i - (len p) as Element of NAT by NAT_1:21;

A58: 1 <= j + 1 by NAT_1:12;

len f = (len q) - (len p) by A23, A26, XCMPLX_1:26;

then A59: j < len f by A57, XREAL_1:9;

then j + 1 <= len f by NAT_1:13;

then j + 1 in Seg (len f) by A58, FINSEQ_1:1;

then A60: (i + 1) - (len p) in Seg (len f) by XCMPLX_1:29;

A61: 1 <= j by A57, XREAL_1:19;

then A62: [(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A59;

then A63: f . ((i - (len p)) + 1) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by ZFMISC_1:87;

A64: for k being Nat st k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) holds

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

A77:
f . (i - (len p)) in the Sorts of A . ((the_arity_of o) /. (n + 1))
by A62, ZFMISC_1:87;
let k be Nat; :: thesis: ( k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )

assume A65: k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A66: ( k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) or ex n1 being Nat st

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

end;assume A65: k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A66: ( k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) or ex n1 being Nat st

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

now :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)end;

hence
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
; :: thesis: verumper cases
( k in dom a2 or ex n2 being Nat st

( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by A66, FINSEQ_1:25;

end;

( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by A66, FINSEQ_1:25;

suppose A67:
k in dom a2
; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then
k in Seg (len a2)
by FINSEQ_1:def 3;

then k in dom a1 by A8, FINSEQ_1:def 3;

then A68: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . ((i + 1) - (len p)))*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A67, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A68, ZFMISC_1:87; :: thesis: verum

end;then k in dom a1 by A8, FINSEQ_1:def 3;

then A68: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . ((i + 1) - (len p)))*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A67, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A68, ZFMISC_1:87; :: thesis: verum

suppose
ex n2 being Nat st

( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n2 being Nat such that

A69: n2 in dom <*(f . ((i + 1) - (len p)))*> and

A70: k = (len a2) + n2 ;

n2 in Seg 1 by A69, FINSEQ_1:38;

then A71: k = (len a1) + 1 by A8, A70, FINSEQ_1:2, TARSKI:def 1;

then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;

then k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:40;

then k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:22;

then k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:def 3;

then ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . ((i + 1) - (len p)))*>) . k by FINSEQ_1:def 7

.= f . ((i + 1) - (len p)) by A8, A71, FINSEQ_1:42 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A63, A71, XCMPLX_1:29; :: thesis: verum

end;A69: n2 in dom <*(f . ((i + 1) - (len p)))*> and

A70: k = (len a2) + n2 ;

n2 in Seg 1 by A69, FINSEQ_1:38;

then A71: k = (len a1) + 1 by A8, A70, FINSEQ_1:2, TARSKI:def 1;

then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;

then k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:40;

then k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:22;

then k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:def 3;

then ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . ((i + 1) - (len p)))*>) . k by FINSEQ_1:def 7

.= f . ((i + 1) - (len p)) by A8, A71, FINSEQ_1:42 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A63, A71, XCMPLX_1:29; :: thesis: verum

suppose A72:
ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A73: len (a1 ^ <*x1*>) =
(len a1) + (len <*x1*>)
by FINSEQ_1:22

.= (len a2) + 1 by A8, FINSEQ_1:40

.= (len a2) + (len <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:40

.= len (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:22 ;

A74: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40

.= Seg (((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:40

.= Seg ((len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1)) by FINSEQ_1:22

.= dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;

consider n1 being Element of NAT such that

A75: n1 in dom b1 and

A76: k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 by A72;

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = b1 . n1 by A75, A76, FINSEQ_1:def 7

.= x . k by A13, A75, A76, A73, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A65, A74; :: thesis: verum

end;.= (len a2) + 1 by A8, FINSEQ_1:40

.= (len a2) + (len <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:40

.= len (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:22 ;

A74: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40

.= Seg (((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:40

.= Seg ((len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1)) by FINSEQ_1:22

.= dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;

consider n1 being Element of NAT such that

A75: n1 in dom b1 and

A76: k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 by A72;

((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = b1 . n1 by A75, A76, FINSEQ_1:def 7

.= x . k by A13, A75, A76, A73, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A65, A74; :: thesis: verum

A78: for k being Nat st k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) holds

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

proof

A92:
1 <= j
by A57, XREAL_1:19;
let k be Nat; :: thesis: ( k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )

assume A79: k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A80: ( k in dom (a2 ^ <*(f . (i - (len p)))*>) or ex n1 being Nat st

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

end;assume A79: k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then A80: ( k in dom (a2 ^ <*(f . (i - (len p)))*>) or ex n1 being Nat st

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;

now :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)end;

hence
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
; :: thesis: verumper cases
( k in dom a2 or ex n2 being Nat st

( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by A80, FINSEQ_1:25;

end;

( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by A80, FINSEQ_1:25;

suppose A81:
k in dom a2
; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then
k in Seg (len a2)
by FINSEQ_1:def 3;

then k in dom a1 by A8, FINSEQ_1:def 3;

then A82: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . (i - (len p)))*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A81, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A82, ZFMISC_1:87; :: thesis: verum

end;then k in dom a1 by A8, FINSEQ_1:def 3;

then A82: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . (i - (len p)))*> ^ b1)) . k by FINSEQ_1:32

.= a2 . k by A81, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A82, ZFMISC_1:87; :: thesis: verum

suppose
ex n2 being Nat st

( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

then consider n2 being Nat such that

A83: n2 in dom <*(f . (i - (len p)))*> and

A84: k = (len a2) + n2 ;

A85: n2 in Seg 1 by A83, FINSEQ_1:38;

then A86: k = (len a1) + 1 by A8, A84, FINSEQ_1:2, TARSKI:def 1;

then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;

then k in Seg ((len a2) + (len <*(f . (i - (len p)))*>)) by FINSEQ_1:40;

then k in Seg (len (a2 ^ <*(f . (i - (len p)))*>)) by FINSEQ_1:22;

then k in dom (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:def 3;

then ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . (i - (len p)))*>) . k by FINSEQ_1:def 7

.= f . (i - (len p)) by A8, A86, FINSEQ_1:42 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A8, A77, A84, A85, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;A83: n2 in dom <*(f . (i - (len p)))*> and

A84: k = (len a2) + n2 ;

A85: n2 in Seg 1 by A83, FINSEQ_1:38;

then A86: k = (len a1) + 1 by A8, A84, FINSEQ_1:2, TARSKI:def 1;

then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;

then k in Seg ((len a2) + (len <*(f . (i - (len p)))*>)) by FINSEQ_1:40;

then k in Seg (len (a2 ^ <*(f . (i - (len p)))*>)) by FINSEQ_1:22;

then k in dom (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:def 3;

then ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . (i - (len p)))*>) . k by FINSEQ_1:def 7

.= f . (i - (len p)) by A8, A86, FINSEQ_1:42 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A8, A77, A84, A85, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

suppose A87:
ex n1 being Element of NAT st

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ; :: thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)

A88: len (a1 ^ <*x1*>) =
(len a1) + (len <*x1*>)
by FINSEQ_1:22

.= (len a2) + 1 by A8, FINSEQ_1:40

.= (len a2) + (len <*(f . (i - (len p)))*>) by FINSEQ_1:40

.= len (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:22 ;

A89: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40

.= Seg (((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:40

.= Seg ((len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1)) by FINSEQ_1:22

.= dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;

consider n1 being Element of NAT such that

A90: n1 in dom b1 and

A91: k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 by A87;

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = b1 . n1 by A90, A91, FINSEQ_1:def 7

.= x . k by A13, A90, A91, A88, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A79, A89; :: thesis: verum

end;.= (len a2) + 1 by A8, FINSEQ_1:40

.= (len a2) + (len <*(f . (i - (len p)))*>) by FINSEQ_1:40

.= len (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:22 ;

A89: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def 3

.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22

.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40

.= Seg (((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:40

.= Seg ((len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:22

.= Seg (len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1)) by FINSEQ_1:22

.= dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) by FINSEQ_1:def 3 ;

consider n1 being Element of NAT such that

A90: n1 in dom b1 and

A91: k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 by A87;

((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = b1 . n1 by A90, A91, FINSEQ_1:def 7

.= x . k by A13, A90, A91, A88, FINSEQ_1:def 7 ;

hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A79, A89; :: thesis: verum

j <= len f by A23, A26, A57, XREAL_1:19;

then A93: i - (len p) in Seg (len f) by A92, FINSEQ_1:1;

A94: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def 3

.= dom (the_arity_of o) by MSUALG_3:6

.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;

A95: len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + 1) + (len b1) by FINSEQ_1:40

.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40

.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22

.= len (the_arity_of o) by A94, FINSEQ_1:6 ;

len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22

.= ((len a2) + 1) + (len b1) by FINSEQ_1:40

.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40

.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22

.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22

.= len (the_arity_of o) by A94, FINSEQ_1:6 ;

then reconsider d1 = (a2 ^ <*(f . (i - (len p)))*>) ^ b1, d2 = (a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as Element of Args (o,A) by A78, A64, A95, MSAFREE2:5;

A96: q . i = g . (i - (len p)) by A26, A57, FINSEQ_1:23

.= (Den (o,A)) . d1 by A23, A24, A93 ;

(i + 1) - (len p) = (i - (len p)) + 1 by XCMPLX_1:29;

then A97: [(f . (i - (len p))),(f . ((i + 1) - (len p)))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A61, A59;

A98: i + 1 <= len q by A57, NAT_1:13;

(len p) + 1 <= i + 1 by A57, NAT_1:12;

then q . (i + 1) = g . ((i + 1) - (len p)) by A26, A98, FINSEQ_1:23

.= (Den (o,A)) . d2 by A23, A24, A60 ;

hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A7, A8, A96, A97, Th12; :: thesis: verum