for n being Nat
for S being Subset-Family of REAL holds Product (n,S) is Subset-Family of (REAL n)