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