theorem :: BINOP_1:17

for X, Y, Z being set
for x, y being object
for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds
f . (x,y) in Z