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;
dom (x,y --> X,Y) = {x,y} by FUNCT_4:65;
then ( x in dom (x,y --> X,Y) & y in dom (x,y --> X,Y) ) by TARSKI:def 2;
then ( f . x in (x,y --> X,Y) . x & f . y in (x,y --> X,Y) . y ) by A2, CARD_3:18;
hence ( f . x in X & f . y in Y ) by A1, FUNCT_4:66; :: thesis: verum