for p being Point of (TOP-REAL 2) holds |.p.| = sqrt (((p `1) ^2) + ((p `2) ^2))