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

now

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