let X, Y be set ; :: thesis: for f, i, j being object st i <> j holds

( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) )

let f, i, j be object ; :: thesis: ( i <> j implies ( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) ) )

assume A1: i <> j ; :: thesis: ( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) )

thus ( f in product ((i,j) --> (X,Y)) implies ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) ) :: thesis: ( ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) implies f in product ((i,j) --> (X,Y)) )

reconsider g = f as Function by A5;

A6: dom g = {i,j} by A5, FUNCT_4:62

.= dom ((i,j) --> (X,Y)) by FUNCT_4:62 ;

for z being object st z in dom ((i,j) --> (X,Y)) holds

g . z in ((i,j) --> (X,Y)) . z

( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) )

let f, i, j be object ; :: thesis: ( i <> j implies ( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) ) )

assume A1: i <> j ; :: thesis: ( f in product ((i,j) --> (X,Y)) iff ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) )

thus ( f in product ((i,j) --> (X,Y)) implies ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) ) :: thesis: ( ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) ) implies f in product ((i,j) --> (X,Y)) )

proof

given x, y being object such that A5:
( x in X & y in Y & f = (i,j) --> (x,y) )
; :: thesis: f in product ((i,j) --> (X,Y))
assume
f in product ((i,j) --> (X,Y))
; :: thesis: ex x, y being object st

( x in X & y in Y & f = (i,j) --> (x,y) )

then consider g being Function such that

A2: ( g = f & dom g = dom ((i,j) --> (X,Y)) ) and

A3: for z being object st z in dom ((i,j) --> (X,Y)) holds

g . z in ((i,j) --> (X,Y)) . z by CARD_3:def 5;

take g . i ; :: thesis: ex y being object st

( g . i in X & y in Y & f = (i,j) --> ((g . i),y) )

take g . j ; :: thesis: ( g . i in X & g . j in Y & f = (i,j) --> ((g . i),(g . j)) )

A4: dom ((i,j) --> (X,Y)) = {i,j} by FUNCT_4:62;

then i in dom ((i,j) --> (X,Y)) by TARSKI:def 2;

then g . i in ((i,j) --> (X,Y)) . i by A3;

hence g . i in X by A1, FUNCT_4:63; :: thesis: ( g . j in Y & f = (i,j) --> ((g . i),(g . j)) )

j in dom ((i,j) --> (X,Y)) by A4, TARSKI:def 2;

then g . j in ((i,j) --> (X,Y)) . j by A3;

hence ( g . j in Y & f = (i,j) --> ((g . i),(g . j)) ) by A2, A4, FUNCT_4:66, FUNCT_4:63; :: thesis: verum

end;( x in X & y in Y & f = (i,j) --> (x,y) )

then consider g being Function such that

A2: ( g = f & dom g = dom ((i,j) --> (X,Y)) ) and

A3: for z being object st z in dom ((i,j) --> (X,Y)) holds

g . z in ((i,j) --> (X,Y)) . z by CARD_3:def 5;

take g . i ; :: thesis: ex y being object st

( g . i in X & y in Y & f = (i,j) --> ((g . i),y) )

take g . j ; :: thesis: ( g . i in X & g . j in Y & f = (i,j) --> ((g . i),(g . j)) )

A4: dom ((i,j) --> (X,Y)) = {i,j} by FUNCT_4:62;

then i in dom ((i,j) --> (X,Y)) by TARSKI:def 2;

then g . i in ((i,j) --> (X,Y)) . i by A3;

hence g . i in X by A1, FUNCT_4:63; :: thesis: ( g . j in Y & f = (i,j) --> ((g . i),(g . j)) )

j in dom ((i,j) --> (X,Y)) by A4, TARSKI:def 2;

then g . j in ((i,j) --> (X,Y)) . j by A3;

hence ( g . j in Y & f = (i,j) --> ((g . i),(g . j)) ) by A2, A4, FUNCT_4:66, FUNCT_4:63; :: thesis: verum

reconsider g = f as Function by A5;

A6: dom g = {i,j} by A5, FUNCT_4:62

.= dom ((i,j) --> (X,Y)) by FUNCT_4:62 ;

for z being object st z in dom ((i,j) --> (X,Y)) holds

g . z in ((i,j) --> (X,Y)) . z

proof

hence
f in product ((i,j) --> (X,Y))
by A6, CARD_3:9; :: thesis: verum
let z be object ; :: thesis: ( z in dom ((i,j) --> (X,Y)) implies g . z in ((i,j) --> (X,Y)) . z )

assume z in dom ((i,j) --> (X,Y)) ; :: thesis: g . z in ((i,j) --> (X,Y)) . z

then z in {i,j} by FUNCT_4:62;

end;assume z in dom ((i,j) --> (X,Y)) ; :: thesis: g . z in ((i,j) --> (X,Y)) . z

then z in {i,j} by FUNCT_4:62;