theorem Th3: :: PRVECT_3:3

for X, Y being non empty set
for D being Function st dom D = {1,2} & D . 1 = X & D . 2 = Y holds
ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )