theorem Th36: :: SRINGS_5:45

for n being Nat
for X being set holds Product (n,X) c= bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X)))))