theorem Th5: :: PRVECT_4:2

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