let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,1) holds
Index (p,f) = 1
let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (f,1) implies Index (p,f) = 1 )
assume A1: p in LSeg (f,1) ; :: thesis: Index (p,f) = 1
then A2: Index (p,f) <= 1 by Th7;
LSeg (f,1) c= L~ f by TOPREAL3:19;
then Index (p,f) >= 1 by A1, Th8;
hence Index (p,f) = 1 by A2, XXREAL_0:1; :: thesis: verum