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