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:25;
hence Rotate <*p*>,p = <*p*> by Th95; :: thesis: verum