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