theorem Th123: :: FINSEQ_3:125

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