let a be Complex; :: 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

then A3: sin (Arg a) = (Im a) / |.a.| by Th24;
set b = a * r;
A4: |.(a * r).| = |.a.| * |.r.| by COMPLEX1:65
.= |.a.| * r by A1, ABSVALUE:def 1 ;
A5: cos (Arg a) = (Re a) / |.a.| by A2, Th24;
A6: ( 0 <= Arg a & Arg a < 2 * PI ) by COMPTRIG:34;
r = r + (0 * <i>) ;
then A7: ( Re r = r & Im r = 0 ) by COMPLEX1:12;
then A8: Im (a * r) = ((Re a) * 0) + (r * (Im a)) by COMPLEX1:9
.= r * (Im a) ;
A9: sin (Arg (a * r)) = (Im (a * r)) / |.(a * r).| by A1, A2, Th24
.= sin (Arg a) by A1, A8, A4, A3, XCMPLX_1:91 ;
A10: ( 0 <= Arg (a * r) & Arg (a * r) < 2 * PI ) by COMPTRIG:34;
A11: Re (a * r) = ((Re a) * r) - (0 * (Im a)) by A7, COMPLEX1:9
.= r * (Re a) ;
cos (Arg (a * r)) = (Re (a * r)) / |.(a * r).| by A1, A2, Th24
.= cos (Arg a) by A1, A11, A4, A5, XCMPLX_1:91 ;
hence Arg (a * r) = Arg a by A9, A10, A6, Th11; :: thesis: verum

end;

end;