deffunc H1( Element of carr f, Element of carr f) -> Element of carr f = multemb (f,$1,$2);
consider F being BinOp of (carr f) such that
A1:
for a, b being Element of carr f holds F . (a,b) = H1(a,b)
from BINOP_1:sch 4();
take
F
; for a, b being Element of carr f holds F . (a,b) = multemb (f,a,b)
thus
for a, b being Element of carr f holds F . (a,b) = multemb (f,a,b)
by A1; verum