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:26;
hence Rotate <*p1,p2*>,p1 = <*p1,p2*> by Th95; :: thesis: verum