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