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

now :: thesis: for a, b being Element of X st (distance_by_norm_of X) . (a,b) = 0 holds
a = b

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 ; :: thesis: verum