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 Th40;
LSeg f,1 c= L~ f by TOPREAL3:26;
then Index p,f >= 1 by A1, Th41;
hence Index p,f = 1 by A2, XXREAL_0:1; :: thesis: verum