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)) . b2 = (((m + 1),r) -cut p) . b2 ) )

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 ;
A5: 1 <= m + 1 by NAT_1:11;
m <= r by ;
then A6: m + 1 <= r + 1 by XREAL_1:6;
A7: m + 1 <= n + 1 by ;
A8: n + 1 <= r + 1 by ;
then m + 1 <= r + 1 by ;
then A9: (len (((m + 1),r) -cut p)) + (m + 1) = r + 1 by A3, A5, Lm2;
A10: n <= len p by ;
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
.= 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)) . b2 = (((m + 1),r) -cut p) . b2

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)) . b1 = (((m + 1),r) -cut p) . b1 )
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)) . b1 = (((m + 1),r) -cut p) . b1
then A15: 1 <= i by ;
A16: i <= len ((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) by ;
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)) . b1 = (((m + 1),r) -cut p) . b1
0 + 1 = 1 ;
then consider k being Nat such that
0 <= k and
A18: k < nm and
A19: i = k + 1 by ;
nm <= r - m by ;
then A20: k < len (((m + 1),r) -cut p) by ;
i in dom (((m + 1),n) -cut p) by ;
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)) . b1 = (((m + 1),r) -cut p) . b1
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 ;
reconsider k99 = k as Integer ;
reconsider k9 = k99 - nm as Element of NAT by ;
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 ;
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 ;
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
.= 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