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 Th29;
hence |.p.| = sqrt (((p `1) ^2) + ((p `2) ^2)) by SQUARE_1:22; :: thesis: verum