let z be Complex; :: thesis: for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))
let r be Real; :: thesis: Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))
thus Rotate (z,(- r)) = (|.z.| * (cos (((2 * PI) * 1) + ((- r) + (Arg z))))) + ((|.z.| * (sin ((- r) + (Arg z)))) * <i>) by COMPLEX2:9
.= Rotate (z,((2 * PI) - r)) by COMPLEX2:8 ; :: thesis: verum