theorem Th97: :: FINSEQ_6:97

for D being non empty set
for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*>