let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st len f >= 2 holds
Index (f /. 1),f = 1
let p be Point of (TOP-REAL 2); :: thesis: ( len f >= 2 implies Index (f /. 1),f = 1 )
assume len f >= 2 ; :: thesis: Index (f /. 1),f = 1
then len f >= 1 + 1 ;
then f /. 1 in LSeg f,1 by TOPREAL1:27;
hence Index (f /. 1),f = 1 by Th43; :: thesis: verum