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:],() 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:],() 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:],() 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 S1[ 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 & S1[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 & S1[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 & S1[x,y,z,w] )

A4: dom <*x,y,z*> = Seg (len <*x,y,z*>) by FINSEQ_1:def 3
.= {1,2,3} by ;
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 ;
hence <*x,y,z*> . i in D . i by ; :: thesis: verum
end;
hence ex w being object st
( w in product D & S1[x,y,z,w] ) by ; :: thesis: verum
end;
consider I being Function of [:X,Y,Z:],() such that
A5: for x, y, z being object st x in X & y in Y & z in Z holds
S1[x,y,z,I . (x,y,z)] from
now :: thesis: not {} in rng Dend;
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 ;
<*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 ;
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 ;
set x = g . 1;
set y = g . 2;
set z = g . 3;
A12: len g = 3 by ;
( 1 in dom D & 2 in dom D & 3 in dom D ) by ;
then A13: ( g . 1 in X & g . 2 in Y & g . 3 in Z & w = <*(g . 1),(g . 2),(g . 3)*> ) by ;
reconsider s = [(g . 1),(g . 2),(g . 3)] as Element of [:X,Y,Z:] by ;
w = I . ((g . 1),(g . 2),(g . 3)) by
.= I . s ;
hence w in rng I by ; :: thesis: verum
end;
then product D c= rng I by TARSKI:def 3;
then I is onto by ;
hence ex I being Function of [:X,Y,Z:],() 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 ; :: thesis: verum