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₁[ 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₁[x,y,z,w] )

proof

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₁[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₁[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 ;

now :: thesis: for i being object st i in dom <*x,y,z*> holds
<*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; :: thesis: verum

end;

hence ex w being object st
( w in product D & S₁[x,y,z,w] ) by A4, A1, CARD_3:9; :: thesis: verum

end;

consider I being Function of [:X,Y,Z:],(product D) such that
A5: for x, y, z being object st x in X & y in Y & z in Z holds
S₁[x,y,z,I . (x,y,z)] from PRVECT_4:sch 1(A2);

now :: thesis: not {} in rng D

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 A6: product D <> {} by CARD_3:26;

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

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;

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

now :: thesis: for w being object st w in product D holds
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;

then product D c= rng I by TARSKI:def 3;
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