for x1, x2 being Real
for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|