theorem :: COMPLEX2:55

for a being Complex holds Rotate (a,(- (Arg a))) = |.a.| by SIN_COS:31;