theorem Th14: :: FINSEQ_6:179

for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Rotate (f,p)) = len f