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