let s be Real; :: thesis: for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))
let p be Point of (TOP-REAL 2); :: thesis: Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))
(Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def 3;
hence Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) by EUCLID_3:1; :: thesis: verum