for p being Point of (TOP-REAL 2) holds
( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) )