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