let X, Y be non empty set ; :: thesis: for D being Function st dom D = {1,2} & D . 1 = X & D . 2 = Y holds
ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
let D be Function; :: thesis: ( dom D = {1,2} & D . 1 = X & D . 2 = Y implies ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) )
assume A1: ( dom D = {1,2} & D . 1 = X & D . 2 = Y ) ; :: thesis: ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
defpred S1[ object , object , object ] means $3 = <*$1,$2*>;
A2: for x, y being object st x in X & y in Y holds
ex z being object st
( z in product D & S1[x,y,z] )
proof
let x, y be object ; :: thesis: ( x in X & y in Y implies ex z being object st
( z in product D & S1[x,y,z] ) )
assume A3: ( x in X & y in Y ) ; :: thesis: ex z being object st
( z in product D & S1[x,y,z] )
A4: dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:2, FINSEQ_1:44 ;
now :: thesis: for i being object st i in dom <*x,y*> holds
<*x,y*> . i in D . i
let i be object ; :: thesis: ( i in dom <*x,y*> implies <*x,y*> . i in D . i )
assume i in dom <*x,y*> ; :: thesis: <*x,y*> . i in D . i
then ( i = 1 or i = 2 ) by A4, TARSKI:def 2;
hence <*x,y*> . i in D . i by A1, A3, FINSEQ_1:44; :: thesis: verum
end;
then <*x,y*> in product D by A4, A1, CARD_3:9;
hence ex z being object st
( z in product D & S1[x,y,z] ) ; :: thesis: verum
end;
consider I being Function of [:X,Y:],(product D) such that
A5: for x, y being object st x in X & y in Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch 1(A2);
now :: thesis: not {} in rng D
assume {} in rng D ; :: thesis: contradiction
then ex x being object st
( x in dom D & D . x = {} ) by FUNCT_1:def 3;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum
end;
then A6: product D <> {} by CARD_3:26;
now :: thesis: for z1, z2 being object st z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume A7: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being object such that
A8: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A9: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by A7, ZFMISC_1:def 2;
<*x1,y1*> = I . (x1,y1) by A5, A8
.= I . (x2,y2) by A7, A8, A9
.= <*x2,y2*> by A5, A9 ;
then ( x1 = x2 & y1 = y2 ) by FINSEQ_1:77;
hence z1 = z2 by A8, A9; :: thesis: verum
end;
then A10: I is one-to-one by A6, FUNCT_2:19;
now :: thesis: for w being object st w in product D holds
w in rng I
let w be object ; :: thesis: ( w in product D implies w in rng I )
assume w in product D ; :: thesis: w in rng I
then consider g being Function such that
A11: ( w = g & dom g = dom D & ( for i being object st i in dom D holds
g . i in D . i ) ) by CARD_3:def 5;
reconsider g = g as FinSequence by A1, A11, FINSEQ_1:2, FINSEQ_1:def 2;
set x = g . 1;
set y = g . 2;
A12: len g = 2 by A1, A11, FINSEQ_1:2, FINSEQ_1:def 3;
( 1 in dom D & 2 in dom D ) by A1, TARSKI:def 2;
then A13: ( g . 1 in X & g . 2 in Y & w = <*(g . 1),(g . 2)*> ) by A11, A12, A1, FINSEQ_1:44;
reconsider z = [(g . 1),(g . 2)] as Element of [:X,Y:] by A13, ZFMISC_1:87;
w = I . ((g . 1),(g . 2)) by A5, A13
.= I . z ;
hence w in rng I by A6, FUNCT_2:112; :: thesis: verum
end;
then product D c= rng I by TARSKI:def 3;
then product D = rng I by XBOOLE_0:def 10;
then I is onto by FUNCT_2:def 3;
hence ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by A5, A10; :: thesis: verum