deffunc H₁( Element of X, Element of X) -> Element of REAL = In (((2 * (f . ($1,$2))) / (((f . ($1,p)) + (f . ($2,p))) + (f . ($1,$2)))),REAL);
ex ff being Function of [:X,X:],REAL st
for x, y being Element of X holds ff . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider fg being Function of [:X,X:],REAL such that
A1: for x, y being Element of X holds fg . (x,y) = H₁(x,y) ;
take fg ; :: thesis: for x, y being Element of X holds fg . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))
let x, y be Element of X; :: thesis: fg . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))
fg . (x,y) = In (((2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y)))),REAL) by A1
.= (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ;
hence fg . (x,y) = (2 * (f . (x,y))) / (((f . (x,p)) + (f . (y,p))) + (f . (x,y))) ; :: thesis: verum