deffunc H₁( Element of A, Element of A) -> Element of REAL = In (((G . ($1,$2)) / (1 + (G . ($1,$2)))),REAL);
consider F being Function of [:A,A:],REAL such that
A1: for a, b being Element of A holds F . (a,b) = H₁(a,b) from BINOP_1:sch 4();
take F ; :: thesis: for a, b being Element of A holds F . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
let a, b be Element of A; :: thesis: F . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
F . (a,b) = H₁(a,b) by A1;
hence F . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ; :: thesis: verum