let a be Complex; :: thesis: Rotate (a,PI) = - a
A1: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) by COMPTRIG:62;
A2: |.a.| * (- (sin (Arg a))) = - (|.a.| * (sin (Arg a)))
.= - (Im a) by A1, COMPLEX1:12 ;
A3: |.a.| * (- (cos (Arg a))) = - (|.a.| * (cos (Arg a)))
.= - (Re a) by A1, COMPLEX1:12 ;
thus Rotate (a,PI) = (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) by SIN_COS:79
.= (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (- (sin (Arg a)))) * <i>) by SIN_COS:79
.= - a by A3, A2, COMPLEX1:83 ; :: thesis: verum