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