theorem Th56: :: JORDAN1J:56
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in rng f & p <> f . 1 holds
(Index (p,f)) + 1 = p .. f