let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ f holds
( 1 <= Index (p,f) & Index (p,f) < len f )
let p be Point of (TOP-REAL 2); ( p in L~ f implies ( 1 <= Index (p,f) & Index (p,f) < len f ) )
assume
p in L~ f
; ( 1 <= Index (p,f) & Index (p,f) < len f )
then consider S being non empty Subset of NAT such that
A1:
Index (p,f) = min S
and
A2:
S = { i where i is Nat : p in LSeg (f,i) }
by Def1;
Index (p,f) in S
by A1, XXREAL_2:def 7;
then A3:
ex i being Nat st
( i = Index (p,f) & p in LSeg (f,i) )
by A2;
hence
1 <= Index (p,f)
by TOPREAL1:def 3; Index (p,f) < len f
(Index (p,f)) + 1 <= len f
by A3, TOPREAL1:def 3;
hence
Index (p,f) < len f
by NAT_1:13; verum