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