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