let D be non

empty set ;

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

p2 be

Element of

D;

Rotate (<*p1,p2*>,p1) = <*p1,p2*>
<*p1,p2*> /. 1

= p1
by FINSEQ_4:17;

hence
Rotate (

<*p1,p2*>,

p1)

= <*p1,p2*>
by Th89;

verum