theorem Th40: :: SRINGS_5:49

for n being non zero Nat
for X being non empty set
for S being non empty Subset-Family of X st S <> {{}} holds
Product (n,S) c= bool (Funcs ((Seg n),X))