thus for f1, f2 being Function of the carrier of BL, the carrier of BL st ( for x being Element of BL holds f1 . x = H₁(x) ) & ( for x being Element of BL holds f2 . x = H₁(x) ) holds
f1 = f2 from BINOP_2:sch 1(); :: thesis: verum