theorem Th4: :: PRVECT_4:1

for X, Y, Z being non empty set
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*> ) )