theorem Th17: :: FINSEQ_6:182

for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))