let X, Y be non empty set ; :: thesis: ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x, y being object st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )
consider J being Function of Y,(product <*Y*>) such that
A1: ( J is one-to-one & J is onto & ( for y being object st y in Y holds
J . y = <*y*> ) ) by PRVECT_3:4;
defpred S₁[ 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 [:X,(product <*Y*>):] & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in X & y in Y implies ex z being object st
( z in [:X,(product <*Y*>):] & S₁[x,y,z] ) )
assume A3: ( x in X & y in Y ) ; :: thesis: ex z being object st
( z in [:X,(product <*Y*>):] & S₁[x,y,z] )
then J . y = <*y*> by A1;
then <*y*> in product <*Y*> by A3, FUNCT_2:5;
hence ex z being object st
( z in [:X,(product <*Y*>):] & S₁[x,y,z] ) by A3, ZFMISC_1:87; :: thesis: verum

end;

consider I being Function of [:X,Y:],[:X,(product <*Y*>):] such that
A4: for x, y being object st x in X & y in Y holds
S₁[x,y,I . (x,y)] from BINOP_1:sch 1(A2);
reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
take I ; :: thesis: ( I is bijective & ( for x, y being object st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )

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 A5: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being object such that
A6: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A7: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by A5, ZFMISC_1:def 2;
[x1,<*y1*>] = I . (x1,y1) by A4, A6
.= I . (x2,y2) by A5, A6, A7
.= [x2,<*y2*>] by A4, A7 ;
then ( x1 = x2 & <*y1*> = <*y2*> ) by XTUPLE_0:1;
hence z1 = z2 by A6, A7, FINSEQ_1:76; :: thesis: verum

end;

then A8: I is one-to-one by FUNCT_2:19;

now :: thesis: for w being object st w in [:X,(product <*Y*>):] holds
w in rng I

let w be object ; :: thesis: ( w in [:X,(product <*Y*>):] implies w in rng I )
assume w in [:X,(product <*Y*>):] ; :: thesis: w in rng I
then consider x, y1 being object such that
A9: ( x in X & y1 in product <*Y*> & w = [x,y1] ) by ZFMISC_1:def 2;
y1 in rng J by A1, A9, FUNCT_2:def 3;
then consider y being object such that
A10: ( y in Y & y1 = J . y ) by FUNCT_2:11;
J . y = <*y*> by A10, A1;
then A11: w = I . (x,y) by A4, A9, A10;
[x,y] in [:X,Y:] by A9, A10, ZFMISC_1:87;
hence w in rng I by A11, FUNCT_2:4; :: thesis: verum

end;

then [:X,(product <*Y*>):] c= rng I by TARSKI:def 3;
then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence ( I is bijective & ( for x, y being object st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) ) by A4, A8; :: thesis: verum