let x, y, X, Y be set ; :: thesis: for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds
( f . x in X & f . y in Y )
let f be Function; :: thesis: ( x <> y & f in product ((x,y) --> (X,Y)) implies ( f . x in X & f . y in Y ) )
assume that
A1: x <> y and
A2: f in product ((x,y) --> (X,Y)) ; :: thesis: ( f . x in X & f . y in Y )
set g = (x,y) --> (X,Y);
A3: dom ((x,y) --> (X,Y)) = {x,y} by FUNCT_4:62;
then y in dom ((x,y) --> (X,Y)) by TARSKI:def 2;
then A4: f . y in ((x,y) --> (X,Y)) . y by A2, CARD_3:9;
x in dom ((x,y) --> (X,Y)) by A3, TARSKI:def 2;
then f . x in ((x,y) --> (X,Y)) . x by A2, CARD_3:9;
hence ( f . x in X & f . y in Y ) by A1, A4, FUNCT_4:63; :: thesis: verum