for s being Real
for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))