let x1, x2 be Real; :: thesis: for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|
let p be Point of (TOP-REAL 2); :: thesis: ( x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) implies p = |[x1,x2]| )
assume ( x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) ) ; :: thesis: p = |[x1,x2]|
then ( x1 = |.(euc2cpx p).| * (cos (Arg (euc2cpx p))) & x2 = |.(euc2cpx p).| * (sin (Arg (euc2cpx p))) ) by Th25;
then euc2cpx p = x1 + (x2 * <i>) by COMPTRIG:62;
then p = cpx2euc (x1 + (x2 * <i>)) by Th2;
hence p = |[x1,x2]| by Th5; :: thesis: verum