theorem Th89: :: FINSEQ_6:89

for D being non empty set
for f being FinSequence of D holds Rotate (f,(f /. 1)) = f