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