let X, Y, Z be non empty set ; :: thesis: ex I being Function of [:X,Y,Z:],(product <*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*> ) )
( dom <*X,Y,Z*> = {1,2,3} & <*X,Y,Z*> . 1 = X & <*X,Y,Z*> . 2 = Y & <*X,Y,Z*> . 3 = Z ) by FINSEQ_1:89, FINSEQ_3:1;
hence ex I being Function of [:X,Y,Z:],(product <*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 Th4; :: thesis: verum