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