let a, b, x, y, X, Y be set ; :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum