let p be FinSequence; 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; ( 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
; (((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 ( 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))
;
( 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 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;
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) . b2let i be
Nat;
( 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))
;
((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b1 = (((m + 1),r) -cut p) . b1then 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
;
((((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 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
;
verum end; suppose
nm + 1
<= i
;
((((m + 1),n) -cut p) ^ (((n + 1),r) -cut p)) . b1 = (((m + 1),r) -cut p) . b1then 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
;
verum end; end; end;
hence
(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p
by FINSEQ_2:9; verum