theorem Th9: :: SPPOL_2:9

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)