let X be non empty set ; :: thesis: for f being nonnegative-yielding Function of [:X,X:],REAL
for p, x, y being Element of X holds (SteinhausGen (f,p)) . (x,y) >= 0
let f be nonnegative-yielding Function of [:X,X:],REAL; :: thesis: for p, x, y being Element of X holds (SteinhausGen (f,p)) . (x,y) >= 0
let p, x, y be Element of X; :: thesis: (SteinhausGen (f,p)) . (x,y) >= 0
set ff = SteinhausGen (f,p);
A1: (SteinhausGen (f,p)) . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) by SteinGen;
A3: f . (x,y) >= 0 by Non;
( f . (x,p) >= 0 & f . (y,p) >= 0 ) by Non;
hence (SteinhausGen (f,p)) . (x,y) >= 0 by A1, A3; :: thesis: verum