theorem Th38: :: SRINGS_5:47

for n being Nat
for X being set
for S being non empty Subset-Family of X holds Product (n,S) = { (product f) where f is Tuple of n,S : verum }