deffunc H₁( Element of A, Element of A) -> Element of REAL = (G . $1,$2) / (1 + (G . $1,$2));
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))
thus F . a,b = (G . a,b) / (1 + (G . a,b)) by A1; :: thesis: verum