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