let x, y, X, Y be set ; 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; ( 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)
; ( 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:65;
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:18;
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:18;
hence
( f . x in X & f . y in Y )
by A1, A4, FUNCT_4:66; verum