let D be non empty set ; 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; 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; verum