let X, Y be non empty set ; :: thesis: ex I being Function of [:X,Y:],[:X,():] 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*>] ) )

A1: product <*Y*> <> {}
proof end;
consider J being Function of Y,() such that
A2: ( 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 S1[ object , object , object ] means \$3 = [\$1,<*\$2*>];
A3: for x, y being object st x in X & y in Y holds
ex z being object st
( z in [:X,():] & 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 [:X,():] & S1[x,y,z] ) )

assume A4: ( x in X & y in Y ) ; :: thesis: ex z being object st
( z in [:X,():] & S1[x,y,z] )

reconsider z = [x,<*y*>] as set by TARSKI:1;
take z ; :: thesis: ( z in [:X,():] & S1[x,y,z] )
J . y = <*y*> by A2, A4;
then <*y*> in product <*Y*> by ;
hence ( z in [:X,():] & S1[x,y,z] ) by ; :: thesis: verum
end;
consider I being Function of [:X,Y:],[:X,():] such that
A5: for x, y being object st x in X & y in Y holds
S1[x,y,I . (x,y)] from reconsider I = I as Function of [:X,Y:],[:X,():] ;
take I ; :: thesis: ( 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*>] ) )

thus I is one-to-one :: thesis: ( I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )
proof
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 A6: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being object such that
A7: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being object such that
A8: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by ;
A9: [x1,<*y1*>] = I . (x1,y1) by A5, A7
.= I . (x2,y2) by A6, A7, A8
.= [x2,<*y2*>] by A5, A8 ;
then <*y1*> = <*y2*> by XTUPLE_0:1;
then y1 = y2 by FINSEQ_1:76;
hence z1 = z2 by ; :: thesis: verum
end;
hence I is one-to-one by ; :: thesis: verum
end;
thus I is onto :: thesis: for x, y being set st x in X & y in Y holds
I . (x,y) = [x,<*y*>]
proof
now :: thesis: for w being object st w in [:X,():] holds
w in rng I
let w be object ; :: thesis: ( w in [:X,():] implies w in rng I )
assume w in [:X,():] ; :: thesis: w in rng I
then consider x, y1 being object such that
A10: ( x in X & y1 in product <*Y*> & w = [x,y1] ) by ZFMISC_1:def 2;
y1 in rng J by ;
then consider y being object such that
A11: ( y in Y & y1 = J . y ) by FUNCT_2:11;
A12: J . y = <*y*> by ;
reconsider z = [x,y] as Element of [:X,Y:] by ;
w = I . (x,y) by A5, A10, A11, A12
.= I . z ;
hence w in rng I by ; :: thesis: verum
end;
then [:X,():] c= rng I by TARSKI:def 3;
hence I is onto by ; :: thesis: verum
end;
thus for x, y being set st x in X & y in Y holds
I . (x,y) = [x,<*y*>] by A5; :: thesis: verum