theorem :: FINSEQ_6:94

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