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

end;

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