deffunc H₁( Element of A) -> object = [$1,y];
thus for f1, f2 being Function of A,[:A,B:] st ( for x being Element of A holds f1 . x = H₁(x) ) & ( for x being Element of A holds f2 . x = H₁(x) ) holds
f1 = f2 from BINOP_2:sch 1(); :: thesis: verum