let z be complex number ; :: 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:10
.= Rotate z,((2 * PI ) - r) by COMPLEX2:9 ; :: thesis: verum