let r be Real; Rotate (- r) = Rotate ((2 * PI) - r)
now for p being Point of (TOP-REAL 2) holds (Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * <i>)),(- r))))]|let p be
Point of
(TOP-REAL 2);
(Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * <i>)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * <i>)),(- r))))]|thus (Rotate ((2 * PI) - r)) . p =
|[(Re (Rotate (((p `1) + ((p `2) * <i>)),((2 * PI) - r)))),(Im (Rotate (((p `1) + ((p `2) * <i>)),((2 * PI) - r))))]|
by Def3
.=
|[(Re (Rotate (((p `1) + ((p `2) * <i>)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * <i>)),((2 * PI) - r))))]|
by Th5
.=
|[(Re (Rotate (((p `1) + ((p `2) * <i>)),(- r)))),(Im (Rotate (((p `1) + ((p `2) * <i>)),(- r))))]|
by Th5
;
verum end;
hence
Rotate (- r) = Rotate ((2 * PI) - r)
by Def3; verum