let p be FinSequence; :: thesis: for m, n, r being Element of 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 Element of 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

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:18;
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:8;
A7: m + 1 <= n + 1 by A1, XREAL_1:8;
A8: n + 1 <= r + 1 by A2, XREAL_1:8;
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:35
.= 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:3;
A16: i <= len (((m + 1),n -cut p) ^ ((n + 1),r -cut p)) by A4, A14, FINSEQ_1:3;

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 Element of 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:11;
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:27;
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 Element of 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:18;
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:35;
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:11;
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:27;
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:10; :: thesis: verum