let f be FinSequence of ; :: thesis: for p being Point of st p in L~ f holds
p in LSeg f,(Index p,f)
let p be Point of ; :: thesis: ( p in L~ f implies p in LSeg f,(Index p,f) )
assume p in L~ f ; :: thesis: p in LSeg f,(Index p,f)
then consider S being non empty Subset of 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 ex i being Element of NAT st
( i = Index p,f & p in LSeg f,i ) by A2;
hence p in LSeg f,(Index p,f) ; :: thesis: verum