let D be non empty set ; :: thesis: for p being Element of D holds Rotate (<*p*>,p) = <*p*>
let p be Element of D; :: thesis: Rotate (<*p*>,p) = <*p*>
<*p*> /. 1 = p by FINSEQ_4:16;
hence Rotate (<*p*>,p) = <*p*> by Th89; :: thesis: verum