let r be Real; :: thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r holds
Arg p = (2 * PI) * (frac r)
let p be Point of (TOP-REAL 2); :: thesis: ( p = CircleMap . r implies Arg p = (2 * PI) * (frac r) )
set z = euc2cpx p;
set A = (2 * PI) * (frac r);
assume A1: p = CircleMap . r ; :: thesis: Arg p = (2 * PI) * (frac r)
reconsider q = CircleMap . (R^1 r) as Point of (TOP-REAL 2) by PRE_TOPC:25;
A2: |.(euc2cpx p).| = |.p.| by EUCLID_3:25;
A3: |.q.| = 1 by TOPREALB:12;
( frac r < 1 & 0 <= frac r ) by INT_1:43;
then A4: ( (2 * PI) * Q <= (2 * PI) * (frac r) & (2 * PI) * (frac r) < (2 * PI) * 1 ) by XREAL_1:68;
A5: ( |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| `1 = cos ((2 * PI) * r) & |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| `2 = sin ((2 * PI) * r) ) by EUCLID:52;
A6: CircleMap . r = |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| by TOPREALB:def 11;
(2 * PI) * (frac r) = ((2 * PI) * r) + ((2 * PI) * (- [\r/])) ;
then ( cos ((2 * PI) * r) = cos ((2 * PI) * (frac r)) & sin ((2 * PI) * r) = sin ((2 * PI) * (frac r)) ) by COMPLEX2:8, COMPLEX2:9;
then euc2cpx p = (|.(euc2cpx p).| * (cos ((2 * PI) * (frac r)))) + ((|.(euc2cpx p).| * (sin ((2 * PI) * (frac r)))) * <i>) by A1, A2, A3, A5, A6;
hence Arg p = (2 * PI) * (frac r) by A4, A2, A1, A3, COMPLEX1:44, COMPTRIG:def 1; :: thesis: verum