theorem Th121: :: FINSEQ_3:123

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