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)) )
proof
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;
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))
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
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;
per cases then ( z = i or z = j ) by TARSKI:def 2;
suppose A7: z = i ; :: thesis: g . z in ((i,j) --> (X,Y)) . z
then g . z = x by A1, A5, FUNCT_4:63;
hence g . z in ((i,j) --> (X,Y)) . z by A1, A5, A7, FUNCT_4:63; :: thesis: verum
end;
suppose A8: z = j ; :: thesis: g . z in ((i,j) --> (X,Y)) . z
then g . z = y by A5, FUNCT_4:63;
hence g . z in ((i,j) --> (X,Y)) . z by A5, A8, FUNCT_4:63; :: thesis: verum
end;
end;
end;
hence f in product ((i,j) --> (X,Y)) by A6, CARD_3:9; :: thesis: verum