theorem Th42: :: SRINGS_5:57

for n being Nat
for S being non empty Subset-Family of REAL
for x being Subset of (REAL n) holds
( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )