let N be Nat; :: thesis: for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0. (TOP-REAL N)
let w be Point of (TOP-REAL N); :: thesis: ( |.w.| = 0 implies w = 0. (TOP-REAL N) )
reconsider s = w as Element of REAL N by EUCLID:22;
assume |.w.| = 0 ; :: thesis: w = 0. (TOP-REAL N)
then s = 0* N by EUCLID:8
.= 0. (TOP-REAL N) by EUCLID:70 ;
hence w = 0. (TOP-REAL N) ; :: thesis: verum