theorem Th37: :: SRINGS_5:46

for n being Nat
for X being set
for S being Subset-Family of X holds Product (n,S) is Subset-Family of (product ((Seg n) --> X))