deffunc H_{1}( Element of T, Element of T) -> Element of T = Tern ($1,x,$2);

consider ff being BinOp of T such that

A1: for a, b being Element of T holds ff . (a,b) = H_{1}(a,b)
from BINOP_1:sch 4();

take ff ; :: thesis: for a, b being Element of T holds ff . (a,b) = Tern (a,x,b)

thus for a, b being Element of T holds ff . (a,b) = Tern (a,x,b) by A1; :: thesis: verum

consider ff being BinOp of T such that

A1: for a, b being Element of T holds ff . (a,b) = H

take ff ; :: thesis: for a, b being Element of T holds ff . (a,b) = Tern (a,x,b)

thus for a, b being Element of T holds ff . (a,b) = Tern (a,x,b) by A1; :: thesis: verum