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;
( (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
;
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;
verum
end;
hence
SteinhausGen (f,p) is discerning
by METRIC_1:def 3; verum