thus for B1, B2 being BinOp of (V .. W) st ( for S1, S2 being Element of V .. W holds B1 . S1,S2 = H₂(S1,S2) ) & ( for S1, S2 being Element of V .. W holds B2 . S1,S2 = H₂(S1,S2) ) holds
B1 = B2 from BINOP_2:sch 2(); :: thesis: verum