for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = |.p.|