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 Element of NAT : p in LSeg f,i } by Def2;
Index p,f in S by A1, XXREAL_2:def 7;
then A3: ex i being Element of NAT st
( i = Index p,f & p in LSeg f,i ) by A2;
hence 1 <= Index p,f by TOPREAL1:def 5; :: thesis: Index p,f < len f
(Index p,f) + 1 <= len f by A3, TOPREAL1:def 5;
hence Index p,f < len f by NAT_1:13; :: thesis: verum