theorem Th5: :: PRVECT_3:5

for X, Y being non empty set ex I being Function of [:X,Y:],(product <*X,Y*>) 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*> ) )