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