let a, b, x, y, X, Y be set ; ( a <> b & x in X & y in Y implies (a,b) --> (x,y) in product ((a,b) --> (X,Y)) )
assume that
A1:
a <> b
and
A2:
( x in X & y in Y )
; (a,b) --> (x,y) in product ((a,b) --> (X,Y))
( {x} c= X & {y} c= Y )
by A2, ZFMISC_1:31;
then
product ((a,b) --> ({x},{y})) c= product ((a,b) --> (X,Y))
by TOPREAL6:21;
then
{((a,b) --> (x,y))} c= product ((a,b) --> (X,Y))
by A1, CARD_3:47;
hence
(a,b) --> (x,y) in product ((a,b) --> (X,Y))
by ZFMISC_1:31; verum