let p be FinSequence; for m, n, a being Nat st a in dom ((m,n) -cut p) holds
ex k being Nat st
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )
let m, n, a be Nat; ( a in dom ((m,n) -cut p) implies ex k being Nat st
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n ) )
assume A1:
a in dom ((m,n) -cut p)
; ex k being Nat st
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )
set cp = (m,n) -cut p;
A2:
a <= len ((m,n) -cut p)
by A1, FINSEQ_3:25;
per cases
( ( 1 <= m & m <= n & n <= len p ) or not 1 <= m or not m <= n or not n <= len p )
;
suppose A3:
( 1
<= m &
m <= n &
n <= len p )
;
ex k being Nat st
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )
0 + 1
<= a
by A1, FINSEQ_3:25;
then consider i1 being
Nat such that
0 <= i1
and A4:
i1 < len ((m,n) -cut p)
and A5:
a = i1 + 1
by A2, FINSEQ_6:127;
take k =
m + i1;
( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )
m <= k
by NAT_1:11;
then A6:
1
<= k
by A3, XXREAL_0:2;
A7:
(len ((m,n) -cut p)) + m = n + 1
by A3, FINSEQ_6:def 4;
A8:
m + i1 < m + (len ((m,n) -cut p))
by A4, XREAL_1:6;
then
m + i1 <= n
by A7, NAT_1:13;
then
k <= len p
by A3, XXREAL_0:2;
hence
k in dom p
by A6, FINSEQ_3:25;
( p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )thus
p . k = ((m,n) -cut p) . a
by A3, A4, A5, FINSEQ_6:def 4;
( k + 1 = m + a & m <= k & k <= n )thus
k + 1
= m + a
by A5;
( m <= k & k <= n )thus
(
m <= k &
k <= n )
by A7, A8, NAT_1:11, NAT_1:13;
verum end;