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:52;
hence Arg (Rotate (c2,(- (Arg c1)))) = 0 by COMPTRIG:def 1; :: thesis: verum