theorem :: FINSEQ_6:176

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)