thus
for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = H_{2}(A,B) ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = H_{2}(A,B) ) holds

b1 = b2 from BINOP_2:sch 2(); :: thesis: verum

b1 = b2 from BINOP_2:sch 2(); :: thesis: verum