deffunc H₁( Element of REAL , Element of Funcs A,REAL ) -> Element of Funcs A,REAL = multreal [;] $1,$2;
consider F being Function of [:REAL ,(Funcs A,REAL ):],(Funcs A,REAL ) such that
A1: for a being Element of REAL
for f being Element of Funcs A,REAL holds F . a,f = H₁(a,f) from BINOP_1:sch 4();
take F ; :: thesis: for a being Real
for f being Element of Funcs A,REAL holds F . a,f = multreal [;] a,f
let a be Real; :: thesis: for f being Element of Funcs A,REAL holds F . a,f = multreal [;] a,f
let f be Element of Funcs A,REAL ; :: thesis: F . a,f = multreal [;] a,f
thus F . a,f = multreal [;] a,f by A1; :: thesis: verum