let a, b be Element of COMPLEX ; :: thesis: for r being Real st r > 0 holds
angle a,b = angle (a * r),(b * r)
let r be Real; :: thesis: ( r > 0 implies angle a,b = angle (a * r),(b * r) )
assume A1: r > 0 ; :: thesis: angle a,b = angle (a * r),(b * r)
then A2: Arg (a * r) = Arg a by Th40;

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

suppose A3: b <> 0 ; :: thesis: angle a,b = angle (a * r),(b * r)

hence angle a,b = Arg (Rotate b,(- (Arg a))) by Def5
.= Arg (Rotate (b * r),(- (Arg (a * r)))) by A1, A2, A3, Th40, Th76
.= angle (a * r),(b * r) by A1, A3, Def5 ;
:: thesis: verum

end;

suppose A4: b = 0 ; :: thesis: angle a,b = angle (a * r),(b * r)

thus angle a,b = angle (a * r),(b * r) :: thesis: verum

proof

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

suppose A5: Arg a = 0 ; :: thesis: angle a,b = angle (a * r),(b * r)

hence angle a,b = Arg (Rotate b,(- (Arg a))) by Def5
.= Arg 0c by A4, Th66
.= Arg (Rotate (b * r),(- (Arg (a * r)))) by A4, Th66
.= angle (a * r),(b * r) by A2, A5, Def5 ;
:: thesis: verum

end;

suppose A6: Arg a <> 0 ; :: thesis: angle a,b = angle (a * r),(b * r)

hence angle a,b = (2 * PI ) - (Arg a) by A4, Def5
.= angle (a * r),(b * r) by A2, A4, A6, Def5 ;
:: thesis: verum

end;

end;

end;

end;

end;