let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)|
let p be Point of (TOP-REAL n); :: thesis: |.p.| = sqrt |(p,p)|
|.p.| = sqrt (|.p.| ^2) by SQUARE_1:22, TOPRNS_1:25
.= sqrt |(p,p)| by Th34 ;
hence |.p.| = sqrt |(p,p)| ; :: thesis: verum