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:37;
then product (a,b --> {x},{y}) c= product (a,b --> X,Y) by TOPREAL6:29;
then {(a,b --> x,y)} c= product (a,b --> X,Y) by A1, CARD_3:63;
hence a,b --> x,y in product (a,b --> X,Y) by ZFMISC_1:37; :: thesis: verum