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