theorem Th39: :: SRINGS_5:48

for X being set
for n being non zero Nat holds Product (n,X) c= bool (Funcs ((Seg n),(union X)))