let r be Real; :: thesis: Rotate (- r) = Rotate ((2 * PI) - r)

now :: thesis: 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); :: thesis: (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 ; :: thesis: verum

end;

hence Rotate (- r) = Rotate ((2 * PI) - r) by Def3; :: thesis: verum