deffunc H₁( Element of PFuncs A,REAL , Element of PFuncs A,REAL ) -> Element of PFuncs A,REAL = $1 (#) $2;
ex F being BinOp of (PFuncs A,REAL ) st
for f, g being Element of PFuncs A,REAL holds F . f,g = H₁(f,g) from BINOP_1:sch 4();
hence ex b₁ being BinOp of (PFuncs A,REAL ) st
for f, g being Element of PFuncs A,REAL holds b₁ . f,g = f (#) g ; :: thesis: verum