deffunc H1( Element of REAL , Element of PFuncs (A,REAL)) -> Element of PFuncs (A,REAL) = $1 (#) $2;
consider F being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) such that
A1:
for a being Element of REAL
for f being Element of PFuncs (A,REAL) holds F . (a,f) = H1(a,f)
from BINOP_1:sch 4();
take
F
; for a being Real
for f being Element of PFuncs (A,REAL) holds F . (a,f) = a (#) f
let a be Real; for f being Element of PFuncs (A,REAL) holds F . (a,f) = a (#) f
let f be Element of PFuncs (A,REAL); F . (a,f) = a (#) f
reconsider a = a as Element of REAL by XREAL_0:def 1;
F . (a,f) = H1(a,f)
by A1;
hence
F . (a,f) = a (#) f
; verum