theorem Th25: :: REVROT_1:25

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