theorem Th31: :: REVROT_1:31

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 & len (f :- p) <= i & i < len f holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))