set A = [.0,1.];
deffunc H₁( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((($1 * $2) / (($1 + $2) - ($1 * $2))),[.0,1.]);
ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st
for x, y being Element of [.0,1.] holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider f being BinOp of [.0,1.] such that
A1: for x, y being Element of [.0,1.] holds f . (x,y) = H₁(x,y) ;
reconsider ff = f as BinOp of [.0,1.] ;
take ff ; :: thesis: for a, b being Element of [.0,1.] holds ff . (a,b) = (a * b) / ((a + b) - (a * b))
let a, b be Element of [.0,1.]; :: thesis: ff . (a,b) = (a * b) / ((a + b) - (a * b))
reconsider aa = a, bb = b as Element of [.0,1.] ;
ff . (a,b) = H₁(aa,bb) by A1;
hence ff . (a,b) = (a * b) / ((a + b) - (a * b)) by SUBSET_1:def 8, HamIn01; :: thesis: verum