set ff = SteinhausGen (f,p);
for a, b being Element of X holds (SteinhausGen (f,p)) . (a,b) = (SteinhausGen (f,p)) . (b,a)
proof
let a,
b be
Element of
X;
(SteinhausGen (f,p)) . (a,b) = (SteinhausGen (f,p)) . (b,a)
(SteinhausGen (f,p)) . (
a,
b) =
(2 * (f . (a,b))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b)))
by SteinGen
.=
(2 * (f . (b,a))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b)))
by METRIC_1:def 4
.=
(2 * (f . (b,a))) / (((f . (b,p)) + (f . (a,p))) + (f . (b,a)))
by METRIC_1:def 4
.=
(SteinhausGen (f,p)) . (
b,
a)
by SteinGen
;
hence
(SteinhausGen (f,p)) . (
a,
b)
= (SteinhausGen (f,p)) . (
b,
a)
;
verum
end;
hence
SteinhausGen (f,p) is symmetric
by METRIC_1:def 4; verum