let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( p in L~ f implies ( 1 <= Index (p,f) & Index (p,f) < len f ) )

assume p in L~ f ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

( 1 <= Index (p,f) & Index (p,f) < len f )

let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( 1 <= Index (p,f) & Index (p,f) < len f ) )

assume p in L~ f ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum