let a, b be 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 Th25;

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 Def3
.= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A1, A2, A3, Th25, Th60
.= angle ((a * r),(b * r)) by A1, A3, Def3 ;
:: 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 Def3
.= Arg 0c by A4, Th50
.= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A4, Th50
.= angle ((a * r),(b * r)) by A2, A5, Def3 ;
:: 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, Def3
.= angle ((a * r),(b * r)) by A2, A4, A6, Def3 ;
:: thesis: verum

end;

end;

end;

end;

end;