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*> <> {}

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 S_{1}[ 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*>):] & S_{1}[x,y,z] )

A5: for x, y being object st x in X & y in Y holds

S_{1}[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*>] ) )

I . (x,y) = [x,<*y*>]

I . (x,y) = [x,<*y*>] by A5; :: thesis: verum

( 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

consider J being Function of Y,(product <*Y*>) such that
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;then {} in rng <*Y*> by CARD_3:26;

then {} in {Y} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

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 S

A3: for x, y being object st x in X & y in Y holds

ex z being object st

( z in [:X,(product <*Y*>):] & S

proof

consider I being Function of [:X,Y:],[:X,(product <*Y*>):] such that
let x, y be object ; :: thesis: ( x in X & y in Y implies ex z being object st

( z in [:X,(product <*Y*>):] & S_{1}[x,y,z] ) )

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

( z in [:X,(product <*Y*>):] & S_{1}[x,y,z] )

reconsider z = [x,<*y*>] as set by TARSKI:1;

take z ; :: thesis: ( z in [:X,(product <*Y*>):] & S_{1}[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*>):] & S_{1}[x,y,z] )
by A4, ZFMISC_1:87; :: thesis: verum

end;( z in [:X,(product <*Y*>):] & S

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

( z in [:X,(product <*Y*>):] & S

reconsider z = [x,<*y*>] as set by TARSKI:1;

take z ; :: thesis: ( z in [:X,(product <*Y*>):] & S

J . y = <*y*> by A2, A4;

then <*y*> in product <*Y*> by A4, A1, FUNCT_2:5;

hence ( z in [:X,(product <*Y*>):] & S

A5: for x, y being object st x in X & y in Y holds

S

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

end;

thus
I is onto
:: thesis: for x, y being set st x in X & y in Y holds now :: thesis: for z1, z2 being object st z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 holds

z1 = z2

hence
I is one-to-one
by FUNCT_2:19, A1; :: thesis: verumz1 = 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;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

I . (x,y) = [x,<*y*>]

proof

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 now :: thesis: for w being object st w in [:X,(product <*Y*>):] holds

w in rng I

then
[:X,(product <*Y*>):] c= rng I
by TARSKI:def 3;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;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

hence I is onto by FUNCT_2:def 3, XBOOLE_0:def 10; :: thesis: verum

I . (x,y) = [x,<*y*>] by A5; :: thesis: verum