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)
A2: Arg (a * r) = Arg a by A1, Th40;

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

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

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

end;

suppose A5: 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 A6: 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 A5, Th66
.= Arg (Rotate (b * r),(- (Arg (a * r)))) by A5, Th66
.= angle (a * r),(b * r) by A2, A6, Def5 ;
:: thesis: verum

end;

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

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

end;

end;

end;

end;

end;