let X, Y, Z be non empty set ; :: thesis: for D being Function st dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z holds

ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) )

let D be Function; :: thesis: ( dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z implies ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) ) )

assume A1: ( dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z ) ; :: thesis: ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) )

defpred S_{1}[ object , object , object , object ] means $4 = <*$1,$2,$3*>;

A2: for x, y, z being object st x in X & y in Y & z in Z holds

ex w being object st

( w in product D & S_{1}[x,y,z,w] )

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

S_{1}[x,y,z,I . (x,y,z)]
from PRVECT_4:sch 1(A2);

then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

hence ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

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

ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) )

let D be Function; :: thesis: ( dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z implies ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) ) )

assume A1: ( dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z ) ; :: thesis: ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

I . (x,y,z) = <*x,y,z*> ) )

defpred S

A2: for x, y, z being object st x in X & y in Y & z in Z holds

ex w being object st

( w in product D & S

proof

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

( w in product D & S_{1}[x,y,z,w] ) )

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

( w in product D & S_{1}[x,y,z,w] )

A4: dom <*x,y,z*> = Seg (len <*x,y,z*>) by FINSEQ_1:def 3

.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;

( w in product D & S_{1}[x,y,z,w] )
by A4, A1, CARD_3:9; :: thesis: verum

end;( w in product D & S

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

( w in product D & S

A4: dom <*x,y,z*> = Seg (len <*x,y,z*>) by FINSEQ_1:def 3

.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;

now :: thesis: for i being object st i in dom <*x,y,z*> holds

<*x,y,z*> . i in D . i

hence
ex w being object st <*x,y,z*> . i in D . i

let i be object ; :: thesis: ( i in dom <*x,y,z*> implies <*x,y,z*> . i in D . i )

assume i in dom <*x,y,z*> ; :: thesis: <*x,y,z*> . i in D . i

then ( i = 1 or i = 2 or i = 3 ) by A4, ENUMSET1:def 1;

hence <*x,y,z*> . i in D . i by A1, A3, FINSEQ_1:45; :: thesis: verum

end;assume i in dom <*x,y,z*> ; :: thesis: <*x,y,z*> . i in D . i

then ( i = 1 or i = 2 or i = 3 ) by A4, ENUMSET1:def 1;

hence <*x,y,z*> . i in D . i by A1, A3, FINSEQ_1:45; :: thesis: verum

( w in product D & S

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

S

now :: thesis: not {} in rng D

then A6:
product D <> {}
by CARD_3:26;assume
{} in rng D
; :: thesis: contradiction

then ex x being object st

( x in dom D & D . x = {} ) by FUNCT_1:def 3;

hence contradiction by A1, ENUMSET1:def 1; :: thesis: verum

end;then ex x being object st

( x in dom D & D . x = {} ) by FUNCT_1:def 3;

hence contradiction by A1, ENUMSET1:def 1; :: thesis: verum

now :: thesis: for w1, w2 being object st w1 in [:X,Y,Z:] & w2 in [:X,Y,Z:] & I . w1 = I . w2 holds

w1 = w2

then A10:
I is one-to-one
by A6, FUNCT_2:19;w1 = w2

let w1, w2 be object ; :: thesis: ( w1 in [:X,Y,Z:] & w2 in [:X,Y,Z:] & I . w1 = I . w2 implies w1 = w2 )

assume A7: ( w1 in [:X,Y,Z:] & w2 in [:X,Y,Z:] & I . w1 = I . w2 ) ; :: thesis: w1 = w2

then consider x1, y1, z1 being object such that

A8: ( x1 in X & y1 in Y & z1 in Z & w1 = [x1,y1,z1] ) by MCART_1:68;

consider x2, y2, z2 being object such that

A9: ( x2 in X & y2 in Y & z2 in Z & w2 = [x2,y2,z2] ) by A7, MCART_1:68;

<*x1,y1,z1*> = I . (x1,y1,z1) by A5, A8

.= I . (x2,y2,z2) by A7, A8, A9

.= <*x2,y2,z2*> by A5, A9 ;

then ( x1 = x2 & y1 = y2 & z1 = z2 ) by FINSEQ_1:78;

hence w1 = w2 by A8, A9; :: thesis: verum

end;assume A7: ( w1 in [:X,Y,Z:] & w2 in [:X,Y,Z:] & I . w1 = I . w2 ) ; :: thesis: w1 = w2

then consider x1, y1, z1 being object such that

A8: ( x1 in X & y1 in Y & z1 in Z & w1 = [x1,y1,z1] ) by MCART_1:68;

consider x2, y2, z2 being object such that

A9: ( x2 in X & y2 in Y & z2 in Z & w2 = [x2,y2,z2] ) by A7, MCART_1:68;

<*x1,y1,z1*> = I . (x1,y1,z1) by A5, A8

.= I . (x2,y2,z2) by A7, A8, A9

.= <*x2,y2,z2*> by A5, A9 ;

then ( x1 = x2 & y1 = y2 & z1 = z2 ) by FINSEQ_1:78;

hence w1 = w2 by A8, A9; :: thesis: verum

now :: thesis: for w being object st w in product D holds

w in rng I

then
product D c= rng I
by TARSKI:def 3;w in rng I

let w be object ; :: 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

A11: ( w = g & dom g = dom D & ( for i being object st i in dom D holds

g . i in D . i ) ) by CARD_3:def 5;

reconsider g = g as FinSequence by A1, A11, FINSEQ_3:1, FINSEQ_1:def 2;

set x = g . 1;

set y = g . 2;

set z = g . 3;

A12: len g = 3 by A1, A11, FINSEQ_1:def 3, FINSEQ_3:1;

( 1 in dom D & 2 in dom D & 3 in dom D ) by A1, ENUMSET1:def 1;

then A13: ( g . 1 in X & g . 2 in Y & g . 3 in Z & w = <*(g . 1),(g . 2),(g . 3)*> ) by A11, A12, A1, FINSEQ_1:45;

reconsider s = [(g . 1),(g . 2),(g . 3)] as Element of [:X,Y,Z:] by A13, MCART_1:69;

w = I . ((g . 1),(g . 2),(g . 3)) by A5, A13

.= I . s ;

hence w in rng I by A6, FUNCT_2:112; :: thesis: verum

end;assume w in product D ; :: thesis: w in rng I

then consider g being Function such that

A11: ( w = g & dom g = dom D & ( for i being object st i in dom D holds

g . i in D . i ) ) by CARD_3:def 5;

reconsider g = g as FinSequence by A1, A11, FINSEQ_3:1, FINSEQ_1:def 2;

set x = g . 1;

set y = g . 2;

set z = g . 3;

A12: len g = 3 by A1, A11, FINSEQ_1:def 3, FINSEQ_3:1;

( 1 in dom D & 2 in dom D & 3 in dom D ) by A1, ENUMSET1:def 1;

then A13: ( g . 1 in X & g . 2 in Y & g . 3 in Z & w = <*(g . 1),(g . 2),(g . 3)*> ) by A11, A12, A1, FINSEQ_1:45;

reconsider s = [(g . 1),(g . 2),(g . 3)] as Element of [:X,Y,Z:] by A13, MCART_1:69;

w = I . ((g . 1),(g . 2),(g . 3)) by A5, A13

.= I . s ;

hence w in rng I by A6, FUNCT_2:112; :: thesis: verum

then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

hence ex I being Function of [:X,Y,Z:],(product D) st

( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds

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