let a, b be Element of COMPLEX ; :: thesis: ( a <> 0 & b <> 0 & Arg a = Arg b implies Arg (- a) = Arg (- b) )
assume ( a <> 0 & b <> 0 & Arg a = Arg b ) ; :: thesis: Arg (- a) = Arg (- b)
then Arg (Rotate a,PI ) = Arg (Rotate b,PI ) by Th76;
then Arg (- a) = Arg (Rotate b,PI ) by Th74;
hence Arg (- a) = Arg (- b) by Th74; :: thesis: verum