let s be Real; :: thesis: 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)
let p be Point of (TOP-REAL 2); :: thesis: ( p <> 0. (TOP-REAL 2) implies ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) )
set c = euc2cpx p;
assume p <> 0. (TOP-REAL 2) ; :: thesis: ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i)
then ex i being Integer st Arg (Rotate ((euc2cpx p),s)) = ((2 * PI) * i) + (s + (Arg (euc2cpx p))) by COMPLEX2:54, EUCLID_3:18;
hence ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) by Th42; :: thesis: verum