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)|
n in NAT by ORDINAL1:def 12;
then |.p.| = sqrt (|.p.| ^2) by SQUARE_1:22, TOPRNS_1:25
.= sqrt |(p,p)| by Th58 ;
hence |.p.| = sqrt |(p,p)| ; :: thesis: verum