let p be FinSequence; :: thesis: for m, n, a being Element of NAT st a in dom (m,n -cut p) holds
ex k being Element of 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 Element of NAT ; :: thesis: ( a in dom (m,n -cut p) implies ex k being Element of 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)
; :: thesis: ex k being Element of 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:
( 1 <= a & a <= len (m,n -cut p) )
by A1, FINSEQ_3:27;
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 )
;
:: thesis: ex k being Element of 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:27;
then consider i1 being
Element of
NAT such that A4:
(
0 <= i1 &
i1 < len (m,n -cut p) &
a = i1 + 1 )
by A2, GRAPH_2:1;
take k =
m + i1;
:: thesis: ( k in dom p & p . k = (m,n -cut p) . a & k + 1 = m + a & m <= k & k <= n )A5:
(len (m,n -cut p)) + m = n + 1
by A3, GRAPH_2:def 1;
A6:
m + i1 < m + (len (m,n -cut p))
by A4, XREAL_1:8;
then A7:
m + i1 <= n
by A5, NAT_1:13;
m <= k
by NAT_1:11;
then
( 1
<= k &
k <= len p )
by A3, A7, XXREAL_0:2;
hence
k in dom p
by FINSEQ_3:27;
:: thesis: ( 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, GRAPH_2:def 1;
:: thesis: ( k + 1 = m + a & m <= k & k <= n )thus
k + 1
= m + a
by A4;
:: thesis: ( m <= k & k <= n )thus
(
m <= k &
k <= n )
by A5, A6, NAT_1:11, NAT_1:13;
:: thesis: verum end;