theorem Th4: :: NDIFF_6:4

for X, Y being non empty set ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x, y being object st x in X & y in Y holds
I . (x,y) = [x,<*y*>] ) )