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)
a in REAL by XREAL_0:def 1;
hence F . (a,f) = multreal [;] (a,f) by A1; :: thesis: verum