let N be Nat; :: thesis: for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
let w1, w2 be Point of (TOP-REAL N); :: thesis: ( w1 = w2 implies |.(w1 - w2).| = 0 )
assume w1 = w2 ; :: thesis: |.(w1 - w2).| = 0
then |.(w1 - w2).| = |.(0. (TOP-REAL N)).| by RLVECT_1:5
.= 0 by Th23 ;
hence |.(w1 - w2).| = 0 ; :: thesis: verum