let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) )
set c = euc2cpx p;
A1: euc2cpx p = (|.(euc2cpx p).| * (cos (Arg (euc2cpx p)))) + ((|.(euc2cpx p).| * (sin (Arg (euc2cpx p)))) * <i>) by COMPTRIG:62;
A2: |.(euc2cpx p).| = |.p.| by EUCLID_3:25;
( Re (euc2cpx p) = p `1 & Im (euc2cpx p) = p `2 ) by COMPLEX1:12;
hence ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) ) by A1, A2, COMPLEX1:12; :: thesis: verum