theorem Th9: :: FINSEQ_6:174

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