theorem Th41: :: SRINGS_5:56
for n being Nat
for S being Subset-Family of REAL holds Product (n,S) is Subset-Family of (REAL n)