for p being Point of (TOP-REAL 3) holds Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2)