let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 = 0 implies Arg (Rotate c2,(- (Arg c1))) = 0 )
assume c2 = 0 ; :: thesis: Arg (Rotate c2,(- (Arg c1))) = 0
then Rotate c2,(- (Arg c1)) = 0 by COMPLEX2:66;
hence Arg (Rotate c2,(- (Arg c1))) = 0 by COMPTRIG:def 1; :: thesis: verum