theorem Th7: :: CAYLDICK:7

for z, X, Y being set st z in product <%X,Y%> holds
ex x, y being set st
( x in X & y in Y & z = <%x,y%> )