let X, Y be non empty set ; :: thesis: ex I being Function of [:X,Y:],[:X,(product <*Y*>):] 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
assume product <*Y*> = {} ; :: thesis: contradiction
then {} in rng <*Y*> by CARD_3:26;
then {} in {Y} by FINSEQ_1:39;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
consider J being Function of Y,(product <*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,(product <*Y*>):] & 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,(product <*Y*>):] & S1[x,y,z] ) )
assume A4: ( x in X & y in Y ) ; :: thesis: ex z being object st
( z in [:X,(product <*Y*>):] & S1[x,y,z] )
reconsider z = [x,<*y*>] as set by TARSKI:1;
take z ; :: thesis: ( z in [:X,(product <*Y*>):] & S1[x,y,z] )
J . y = <*y*> by A2, A4;
then <*y*> in product <*Y*> by A4, A1, FUNCT_2:5;
hence ( z in [:X,(product <*Y*>):] & S1[x,y,z] ) by A4, ZFMISC_1:87; :: thesis: verum
end;
consider I being Function of [:X,Y:],[:X,(product <*Y*>):] 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(A3);
 reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
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 A6, ZFMISC_1:def 2;
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 A7, A8, A9, XTUPLE_0:1; :: thesis: verum
end;
hence I is one-to-one by FUNCT_2:19, A1; :: 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,(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
A10: ( x in X & y1 in product <*Y*> & w = [x,y1] ) by ZFMISC_1:def 2;
y1 in rng J by A2, A10, FUNCT_2:def 3;
then consider y being object such that
A11: ( y in Y & y1 = J . y ) by FUNCT_2:11;
A12: J . y = <*y*> by A11, A2;
reconsider z = [x,y] as Element of [:X,Y:] by A10, A11, ZFMISC_1:87;
w = I . (x,y) by A5, A10, A11, A12
.= I . z ;
hence w in rng I by FUNCT_2:4, A1; :: thesis: verum
end;
then [:X,(product <*Y*>):] c= rng I by TARSKI:def 3;
hence I is onto by FUNCT_2:def 3, XBOOLE_0:def 10; :: 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