theorem Th103: :: FINSEQ_6:103

for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)