theorem :: BINOP_1:19

for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( f is constant iff for x1, x2, y1, y2 being object st x1 in X & x2 in X & y1 in Y & y2 in Y holds
f . (x1,y1) = f . (x2,y2) )