let n be non zero Nat; :: thesis: 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)
let X be non empty set ; :: thesis: for S being non empty Subset-Family of X st S <> {{}} holds
union (Product (n,S)) c= Funcs ((Seg n),X)
let S be non empty Subset-Family of X; :: thesis: ( S <> {{}} implies union (Product (n,S)) c= Funcs ((Seg n),X) )
assume S <> {{}} ; :: thesis: union (Product (n,S)) c= Funcs ((Seg n),X)
then union (Product (n,S)) c= union (bool (Funcs ((Seg n),X))) by ZFMISC_1:77, Th40;
hence union (Product (n,S)) c= Funcs ((Seg n),X) by ZFMISC_1:81; :: thesis: verum