for x, y, X, Y being set
for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds
( f . x in X & f . y in Y )