for s being Real
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i)