:: deftheorem defines = BINOP_1:def 21 :
for X, Y, Z being set
for f1, f2 being Function of [:X,Y:],Z holds
( f1 = f2 iff for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) );