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

proof

let a be Element of X; :: thesis: (SteinhausGen (f,p)) . (a,a) = 0
(SteinhausGen (f,p)) . (a,a) = (2 * (f . (a,a))) / (((f . (a,p)) + (f . (a,p))) + (f . (a,a))) by SteinGen
.= (2 * 0) / (((f . (a,p)) + (f . (a,p))) + (f . (a,a))) by METRIC_1:def 2
.= 0 ;
hence (SteinhausGen (f,p)) . (a,a) = 0 ; :: thesis: verum

end;

hence SteinhausGen (f,p) is Reflexive by METRIC_1:def 2; :: thesis: verum