deffunc H₁( 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<sub>1</sub>(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