deffunc H₁( 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) = H₁(a,f) from BINOP_1:sch 4();
take F ; :: thesis: for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds F . (a,f) = a (#) f
let a be Complex; :: thesis: 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; :: thesis: verum