theorem Th24: :: REVROT_1:24

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