theorem Th29: :: TOPS_5:29

for X, Y being set
for f, i, j being object st i <> j holds
( f in product ((i,j) --> (X,Y)) iff ex x, y being object st
( x in X & y in Y & f = (i,j) --> (x,y) ) )