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