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 p1 = (m + 1),n -cut p;
set p2 = (n + 1),r -cut p;
set p3 = (m + 1),r -cut p;
set p12 = ((m + 1),n -cut p) ^ ((n + 1),r -cut p);
now A4:
( 1
<= m + 1 &
m + 1
<= n + 1 &
n <= len p )
by A1, A2, A3, NAT_1:11, XREAL_1:8, XXREAL_0:2;
then A5:
(len ((m + 1),n -cut p)) + (m + 1) = n + 1
by Lm2;
A6:
( 1
<= n + 1 &
n + 1
<= r + 1 )
by A2, NAT_1:11, XREAL_1:8;
then A7:
(len ((n + 1),r -cut p)) + (n + 1) = r + 1
by A3, Lm2;
m <= r
by A1, A2, XXREAL_0:2;
then A8:
m + 1
<= r + 1
by XREAL_1:8;
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 ) )A9:
len (((m + 1),n -cut p) ^ ((n + 1),r -cut p)) =
(n - m) + (r + (- n))
by A5, A7, FINSEQ_1:35
.=
r - m
;
m + 1
<= r + 1
by A4, A6, XXREAL_0:2;
then A10:
(len ((m + 1),r -cut p)) + (m + 1) = r + 1
by A3, A4, Lm2;
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) . b2X:
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;
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
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) . b1then A11:
( 1
<= i &
i <= len (((m + 1),n -cut p) ^ ((n + 1),r -cut p)) )
by X, FINSEQ_1:3;
reconsider m' =
m as
Integer ;
reconsider n' =
n as
Integer ;
reconsider nm =
n' - m' as
Element of
NAT by A1, INT_1:18;
per cases
( i <= nm or nm + 1 <= i )
by NAT_1:13;
suppose A12:
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
Element of
NAT such that A13:
(
0 <= k &
k < nm &
i = k + 1 )
by A11, A12, Th1;
nm <= r - m
by A2, XREAL_1:11;
then A14:
k < len ((m + 1),r -cut p)
by A10, A13, XXREAL_0:2;
i in dom ((m + 1),n -cut p)
by A5, A11, A12, 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 A4, A5, A13, Lm2
.=
((m + 1),r -cut p) . i
by A3, A4, A8, A13, A14, 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) . b1then consider k being
Element of
NAT such that A15:
(
nm <= k &
k < len (((m + 1),n -cut p) ^ ((n + 1),r -cut p)) &
i = k + 1 )
by A11, Th1;
reconsider k'' =
k as
Integer ;
reconsider k' =
k'' - nm as
Element of
NAT by A15, INT_1:18;
A16:
i = nm + (k' + 1)
by A15;
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 A17:
k' < len ((n + 1),r -cut p)
by A5, A15, XREAL_1:11;
then
( 1
<= k' + 1 &
k' + 1
<= len ((n + 1),r -cut p) )
by NAT_1:11, NAT_1:13;
then A18:
k' + 1
in dom ((n + 1),r -cut p)
by FINSEQ_3:27;
A19:
(n + 1) + k' = (m + 1) + k
;
thus (((m + 1),n -cut p) ^ ((n + 1),r -cut p)) . i =
((n + 1),r -cut p) . (k' + 1)
by A5, A16, A18, FINSEQ_1:def 7
.=
p . ((n + 1) + k')
by A3, A6, A17, Lm2
.=
((m + 1),r -cut p) . i
by A3, A4, A8, A9, A10, A15, A19, Lm2
;
:: thesis: verum end; end;
hence
((m + 1),n -cut p) ^ ((n + 1),r -cut p) = (m + 1),r -cut p
by FINSEQ_2:10; :: thesis: verum