let p be FinSequence; :: thesis: for m, n, r being Nat st m <= n & n <= r & r <= len p holds
(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p
let m, n, r be Nat; :: thesis: ( m <= n & n <= r & r <= len p implies (((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p )
assume that
A1: m <= n and
A2: n <= r and
A3: r <= len p ; :: thesis: (((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p
set p3 = ((m + 1),r) -cut p;
set p2 = ((n + 1),r) -cut p;
set p1 = ((m + 1),n) -cut p;
set p12 = (((m + 1),n) -cut p) ^ (((n + 1),r) -cut p);

now :: thesis: ( len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) = len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) & len (((m + 1),r) -cut p) = len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) & ( for i being Nat st i in dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) holds
((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . i = (((m + 1),r) -cut p) . i ) )

reconsider n9 = n as Integer ;
reconsider m9 = m as Integer ;
thus len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) = len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) ; :: thesis: ( len (((m + 1),r) -cut p) = len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) & ( for i being Nat st i in dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) holds
((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₂ = (((m + 1),r) -cut p) . b₂ ) )
A4: dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) = Seg (len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p))) by FINSEQ_1:def 3;
reconsider nm = n9 - m9 as Element of NAT by A1, INT_1:5;
A5: 1 <= m + 1 by NAT_1:11;
m <= r by A1, A2, XXREAL_0:2;
then A6: m + 1 <= r + 1 by XREAL_1:6;
A7: m + 1 <= n + 1 by A1, XREAL_1:6;
A8: n + 1 <= r + 1 by A2, XREAL_1:6;
then m + 1 <= r + 1 by A7, XXREAL_0:2;
then A9: (len (((m + 1),r) -cut p)) + (m + 1) = r + 1 by A3, A5, Lm2;
A10: n <= len p by A2, A3, XXREAL_0:2;
then A11: (len (((m + 1),n) -cut p)) + (m + 1) = n + 1 by A5, A7, Lm2;
A12: 1 <= n + 1 by NAT_1:11;
then (len (((n + 1),r) -cut p)) + (n + 1) = r + 1 by A3, A8, Lm2;
then A13: len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) = (n - m) + (r + (- n)) by A11, FINSEQ_1:22
.= r - m ;
hence len (((m + 1),r) -cut p) = len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) by A9; :: thesis: for i being Nat st i in dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) holds
((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₂ = (((m + 1),r) -cut p) . b₂
let i be Nat; :: thesis: ( i in dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) implies ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₁ = (((m + 1),r) -cut p) . b₁ )
assume A14: i in dom ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) ; :: thesis: ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₁ = (((m + 1),r) -cut p) . b₁
then A15: 1 <= i by A4, FINSEQ_1:1;
A16: i <= len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) by A4, A14, FINSEQ_1:1;

per cases ( i <= nm or nm + 1 <= i ) by NAT_1:13;

suppose A17: i <= nm ; :: thesis: ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₁ = (((m + 1),r) -cut p) . b₁

0 + 1 = 1 ;
then consider k being Nat such that
0 <= k and
A18: k < nm and
A19: i = k + 1 by A15, A17, Th1;
nm <= r - m by A2, XREAL_1:9;
then A20: k < len (((m + 1),r) -cut p) by A9, A18, XXREAL_0:2;
i in dom (((m + 1),n) -cut p) by A11, A15, A17, FINSEQ_3:25;
hence ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . i = (((m + 1),n) -cut p) . i by FINSEQ_1:def 7
.= p . ((m + 1) + k) by A5, A7, A10, A11, A18, A19, Lm2
.= (((m + 1),r) -cut p) . i by A3, A5, A6, A19, A20, Lm2 ;
:: thesis: verum

end;

suppose nm + 1 <= i ; :: thesis: ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b₁ = (((m + 1),r) -cut p) . b₁

then consider k being Nat such that
A21: nm <= k and
A22: k < len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) and
A23: i = k + 1 by A16, Th1;
reconsider k99 = k as Integer ;
reconsider k9 = k99 - nm as Element of NAT by A21, INT_1:5;
A24: 1 <= k9 + 1 by NAT_1:11;
len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) = (len (((n + 1),r) -cut p)) + (len (((m + 1),n) -cut p)) by FINSEQ_1:22;
then len (((n + 1),r) -cut p) = (len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p))) - (len (((m + 1),n) -cut p)) ;
then A25: k9 < len (((n + 1),r) -cut p) by A11, A22, XREAL_1:9;
then k9 + 1 <= len (((n + 1),r) -cut p) by NAT_1:13;
then A26: k9 + 1 in dom (((n + 1),r) -cut p) by A24, FINSEQ_3:25;
A27: (n + 1) + k9 = (m + 1) + k ;
i = nm + (k9 + 1) by A23;
hence ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . i = (((n + 1),r) -cut p) . (k9 + 1) by A11, A26, FINSEQ_1:def 7
.= p . ((n + 1) + k9) by A3, A12, A8, A25, Lm2
.= (((m + 1),r) -cut p) . i by A3, A5, A6, A13, A9, A22, A23, A27, Lm2 ;
:: thesis: verum

end;

end;

end;

hence (((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p by FINSEQ_2:9; :: thesis: verum