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:21;
hence Index ((f /. 1),f) = 1 by Th10; :: thesis: verum