let X be RealNormSpace; :: thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning

now

let a, b be Element of X; :: thesis: ( (distance_by_norm_of X) . (a,b) = 0 implies a = b )
assume A1: (distance_by_norm_of X) . (a,b) = 0 ; :: thesis: a = b
(distance_by_norm_of X) . (a,b) = ||.(a - b).|| by Def1;
hence a = b by A1, NORMSP_1:6; :: thesis: verum

end;

hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning by METRIC_1:def 3; :: thesis: verum