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;
r = r + (0 * <i> ) ;
then A4: ( Re r = r & Im r = 0 ) by COMPLEX1:28;
then A5: Re (a * r) = ((Re a) * r) - (0 * (Im a)) by COMPLEX1:24
.= r * (Re a) ;
A6: Im (a * r) = ((Re a) * 0 ) + (r * (Im a)) by A4, COMPLEX1:24
.= r * (Im a) ;
A7: |.(a * r).| = |.a.| * (abs r) by COMPLEX1:151
.= |.a.| * r by A1, ABSVALUE:def 1 ;
A9: ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) by A2, Th39;
A10: cos (Arg (a * r)) = (Re (a * r)) / |.(a * r).| by A2, Th39, A1
.= cos (Arg a) by A1, A5, A7, A9, XCMPLX_1:92 ;
A11: sin (Arg (a * r)) = (Im (a * r)) / |.(a * r).| by A2, Th39, A1
.= sin (Arg a) by A1, A6, A7, A9, XCMPLX_1:92 ;
( 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 A10, A11, Th12; :: thesis: verum

end;

end;