theorem Th95: :: FINSEQ_6:95

for D being non empty set
for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p1) = <*p1,p2*>