theorem Th10: :: SPPOL_2:10

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