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

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