theorem :: FINSEQ_6:99

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