let p be FinSequence; for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
let m, n be Nat; ( 1 <= m & m <= n + 1 & n <= len p implies ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) ) )
assume that
A1:
1 <= m
and
A2:
m <= n + 1
and
A3:
n <= len p
; ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
A4:
( m = n + 1 or m < n + 1 )
by A2, XXREAL_0:1;
per cases
( m = n + 1 or m <= n )
by A4, NAT_1:13;
suppose A5:
m = n + 1
;
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )then A6:
n < m
by XREAL_1:29;
A7:
( not 1
<= m or not
m <= n or not
n <= len p )
by A5, XREAL_1:29;
(
m,
n)
-cut p = {}
by A6, FINSEQ_6:def 4;
hence
(len ((m,n) -cut p)) + m = n + 1
by A5;
for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i)thus
for
i being
Nat st
i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i)
by A7, CARD_1:27, FINSEQ_6:def 4;
verum end; end;