theorem Th15: :: GROUP_14:15

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