theorem Th8: :: SPRECT_5:8

for f being constant standard special_circular_sequence
for q being Point of (TOP-REAL 2) st 1 < q .. f & q in rng f holds
(f /. 1) .. (Rotate (f,q)) = ((len f) + 1) - (q .. f)