theorem Th32: :: REVROT_1:32

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