theorem :: BORSUK_7:34

for p being Point of (TOP-REAL 3) holds sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*>