let n be 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)
let X be 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 S be non empty Subset-Family of X; ( S <> {{}} implies union (Product (n,S)) c= Funcs ((Seg n),X) )
assume
S <> {{}}
; 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; verum