let f be FinSequence of ; :: thesis: for p being Point of st len f >= 2 holds
Index (f /. 1),f = 1
let p be Point of ; :: 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