deffunc H_{1}( Element of carr (x,o), Element of carr (x,o)) -> Element of carr (x,o) = addR ($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_{1}(a,b)
from BINOP_1:sch 4();

take F ; :: thesis: for a, b being Element of carr (x,o) holds F . (a,b) = addR (a,b)

let a, b be Element of carr (x,o); :: thesis: F . (a,b) = addR (a,b)

thus F . (a,b) = addR (a,b) by A1; :: thesis: verum

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

take F ; :: thesis: for a, b being Element of carr (x,o) holds F . (a,b) = addR (a,b)

let a, b be Element of carr (x,o); :: thesis: F . (a,b) = addR (a,b)

thus F . (a,b) = addR (a,b) by A1; :: thesis: verum