let p be Point of (TOP-REAL 3); :: thesis: sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*>
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3;
hence sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*> by Th15; :: thesis: verum