let p be Point of (TOP-REAL 2); :: thesis: |.p.| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))
|.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by Th46;
hence |.p.| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by SQUARE_1:89; :: thesis: verum