theorem Th122: :: FINSEQ_3:124

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