let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) )
assume A1: p in L~ f ; :: thesis: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))
then Index p,f < len f by JORDAN3:41;
then A2: ( 1 <= Index p,f & (Index p,f) + 1 <= len f ) by A1, JORDAN3:41, NAT_1:13;
p in LSeg f,(Index p,f) by A1, JORDAN3:42;
hence p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, TOPREAL1:def 5; :: thesis: verum