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

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