set ff = SteinhausGen (f,p);
for a, b being Element of X st (SteinhausGen (f,p)) . (a,b) = 0 holds
a = b

proof

let a, b be Element of X; :: thesis: ( (SteinhausGen (f,p)) . (a,b) = 0 implies a = b )
( f . (a,p) >= 0 & f . (b,p) >= 0 ) by Non;
then A0: ( (f . (a,p)) + (f . (b,p)) >= 0 & f . (a,b) >= 0 ) by Non;
assume A1: (SteinhausGen (f,p)) . (a,b) = 0 ; :: thesis: a = b
(SteinhausGen (f,p)) . (a,b) = (2 * (f . (a,b))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b))) by SteinGen;
then ( f . (a,b) = 0 or ( (f . (a,p)) + (f . (b,p)) = 0 & f . (a,b) = 0 ) ) by A0, A1;
hence a = b by METRIC_1:def 3; :: thesis: verum

end;

hence SteinhausGen (f,p) is discerning by METRIC_1:def 3; :: thesis: verum