let RNS be RealNormSpace; :: thesis: for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )
let x, y be Point of RNS; :: thesis: ( ||.(x - y).|| = 0 iff x = y )
( ||.(x - y).|| = 0 iff x - y = H₁(RNS) ) by NORMSP_0:def 5;
hence ( ||.(x - y).|| = 0 iff x = y ) by RLVECT_1:15, RLVECT_1:21; :: thesis: verum