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;