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 A2: Index (p,f) < len f by JORDAN3:8;
A3: 1 <= Index (p,f) by A1, JORDAN3:8;
A4: (Index (p,f)) + 1 <= len f by A2, NAT_1:13;
p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9;
hence p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A4, TOPREAL1:def 3; :: thesis: verum