deffunc H₁( Real, Real) -> set = (h ") . (f . ((h . $1),(h . $2)));
reconsider A = [.0,1.] as non empty real-membered set ;
for o1, o2 being BinOp of A st ( for a, b being Element of A holds o1 . (a,b) = H₁(a,b) ) & ( for a, b being Element of A holds o2 . (a,b) = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2();
hence for b₁, b₂ being BinOp of [.0,1.] st ( for x1, x2 being Element of [.0,1.] holds b₁ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) & ( for x1, x2 being Element of [.0,1.] holds b₂ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) holds
b₁ = b₂ ; :: thesis: verum