let n be Element of NAT ; :: thesis: for f being FinSequence of (TOP-REAL 2)
for x being set st n <= len f & x in L~ (f /^ n) holds
ex i being Element of NAT st
( n + 1 <= i & i + 1 <= len f & x in LSeg f,i )
let f be FinSequence of (TOP-REAL 2); :: thesis: for x being set st n <= len f & x in L~ (f /^ n) holds
ex i being Element of NAT st
( n + 1 <= i & i + 1 <= len f & x in LSeg f,i )
let x be set ; :: thesis: ( n <= len f & x in L~ (f /^ n) implies ex i being Element of NAT st
( n + 1 <= i & i + 1 <= len f & x in LSeg f,i ) )
assume that
A1: n <= len f and
A2: x in L~ (f /^ n) ; :: thesis: ex i being Element of NAT st
( n + 1 <= i & i + 1 <= len f & x in LSeg f,i )
consider j being Element of NAT such that
A3: 1 <= j and
A4: j + 1 <= len (f /^ n) and
A5: x in LSeg (f /^ n),j by A2, SPPOL_2:13;
A6: j + 1 <= (len f) - n by A1, A4, RFINSEQ:def 2;
take n + j ; :: thesis: ( n + 1 <= n + j & (n + j) + 1 <= len f & x in LSeg f,(n + j) )
j + 1 <= (len f) - n by A1, A4, RFINSEQ:def 2;
then n + (j + 1) <= len f by XREAL_1:21;
hence ( n + 1 <= n + j & (n + j) + 1 <= len f & x in LSeg f,(n + j) ) by A3, A5, A6, SPPOL_2:5, XREAL_1:8; :: thesis: verum