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 set 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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) )
assume AS: ( 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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
defpred S₁[ set , set , set ] means $3 = <*$1,$2*>;
P1: for x, y being set st x in X & y in Y holds
ex z being set st
( z in product D & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in X & y in Y implies ex z being set st
( z in product D & S₁[x,y,z] ) )
assume AS0: ( x in X & y in Y ) ; :: thesis: ex z being set st
( z in product D & S₁[x,y,z] )
X0: dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:4, FINSEQ_1:61 ;

now

let i be set ; :: 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 X0, TARSKI:def 2;
hence <*x,y*> . i in D . i by AS, AS0, FINSEQ_1:61; :: thesis: verum

end;

then <*x,y*> in product D by X0, AS, CARD_3:18;
hence ex z being set st
( z in product D & S₁[x,y,z] ) ; :: thesis: verum

end;

consider I being Function of [:X,Y:],(product D) such that
P2: for x, y being set st x in X & y in Y holds
S₁[x,y,I . (x,y)] from BINOP_1:sch 1(P1);

now

assume {} in rng D ; :: thesis: contradiction
then ex x being set st
( x in dom D & D . x = {} ) by FUNCT_1:def 5;
hence contradiction by AS, TARSKI:def 2; :: thesis: verum

end;

then A6: product D <> {} by CARD_3:37;

now

let z1, z2 be set ; :: thesis: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume P3: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being set such that
P4: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being set such that
P5: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by ZFMISC_1:def 2, P3;
<*x1,y1*> = I . (x1,y1) by P2, P4
.= I . (x2,y2) by P3, P4, P5
.= <*x2,y2*> by P2, P5 ;
then ( x1 = x2 & y1 = y2 ) by FINSEQ_1:98;
hence z1 = z2 by P4, P5; :: thesis: verum

end;

then P3: I is one-to-one by A6, FUNCT_2:25;

now

let w be set ; :: 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
X1: ( w = g & dom g = dom D & ( for i being set st i in dom D holds
g . i in D . i ) ) by CARD_3:def 5;
reconsider g = g as FinSequence by AS, X1, FINSEQ_1:4, FINSEQ_1:def 2;
set x = g . 1;
set y = g . 2;
X3: len g = 2 by AS, X1, FINSEQ_1:4, FINSEQ_1:def 3;
( 1 in dom D & 2 in dom D ) by AS, TARSKI:def 2;
then P40: ( g . 1 in X & g . 2 in Y & w = <*(g . 1),(g . 2)*> ) by X1, X3, AS, FINSEQ_1:61;
reconsider z = [(g . 1),(g . 2)] as Element of [:X,Y:] by P40, ZFMISC_1:106;
w = I . ((g . 1),(g . 2)) by P2, P40
.= I . z ;
hence w in rng I by A6, FUNCT_2:189; :: 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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by P2, P3; :: thesis: verum