let a be complex number ; :: thesis: for r being Real st r < 0 holds
Arg (a * r) = Arg (- a)
let r be Real; :: thesis: ( r < 0 implies Arg (a * r) = Arg (- a) )
assume A1: r < 0 ; :: thesis: Arg (a * r) = Arg (- a)

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: Arg (a * r) = Arg (- a)

hence Arg (a * r) = Arg (- a) ; :: thesis: verum

end;

suppose A2: a <> 0 ; :: thesis: Arg (a * r) = Arg (- a)

set b = a * r;
A3: ( a in COMPLEX & a * r in COMPLEX ) by XCMPLX_0:def 2;
r = r + (0 * <i> ) ;
then A5: ( Re r = r & Im r = 0 ) by COMPLEX1:28;
then A6: Re (a * r) = ((Re a) * r) - (0 * (Im a)) by COMPLEX1:24
.= r * (Re a) ;
A7: Im (a * r) = ((Re a) * 0 ) + (r * (Im a)) by A5, COMPLEX1:24
.= r * (Im a) ;
A8: |.(a * r).| = |.a.| * (abs r) by COMPLEX1:151
.= |.a.| * (- r) by A1, ABSVALUE:def 1 ;
A11: ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) by A2, Th39;
A12: cos (Arg (a * r)) = (r * (Re a)) / (- (|.a.| * r)) by A6, A8, A2, Th39, A1
.= - ((r * (Re a)) / (|.a.| * r)) by XCMPLX_1:189
.= - (cos (Arg a)) by A1, A11, XCMPLX_1:92
.= cos (Arg (- a)) by A2, A3, Th38 ;
A13: sin (Arg (a * r)) = (r * (Im a)) / (- (|.a.| * r)) by A7, A8, A2, Th39, A1
.= - ((r * (Im a)) / (|.a.| * r)) by XCMPLX_1:189
.= - (sin (Arg a)) by A1, A11, XCMPLX_1:92
.= sin (Arg (- a)) by A2, A3, Th38 ;
( 0 <= Arg (a * r) & Arg (a * r) < 2 * PI & 0 <= Arg (- a) & Arg (- a) < 2 * PI ) by COMPTRIG:52;
hence Arg (a * r) = Arg (- a) by A12, A13, Th12; :: thesis: verum

end;

end;