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