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
Product (n,S) c= bool (Funcs ((Seg n),X))
let X be non empty set ; :: thesis: for S being non empty Subset-Family of X st S <> {{}} holds
Product (n,S) c= bool (Funcs ((Seg n),X))
let S be non empty Subset-Family of X; :: thesis: ( S <> {{}} implies Product (n,S) c= bool (Funcs ((Seg n),X)) )
assume A1: S <> {{}} ; :: thesis: Product (n,S) c= bool (Funcs ((Seg n),X))
A2: Product (n,S) c= bool (Funcs ((Seg n),(union S))) by Th39;
union S c= union (bool X) by ZFMISC_1:77;
then A3: union S is non empty Subset of X by A1, ZFMISC_1:81, SCMYCIEL:18;
( n -tuples_on X = Funcs ((Seg n),X) & n -tuples_on (union S) = Funcs ((Seg n),(union S)) ) by FINSEQ_2:93;
then bool (Funcs ((Seg n),(union S))) c= bool (Funcs ((Seg n),X)) by A3, Th5, ZFMISC_1:67;
hence Product (n,S) c= bool (Funcs ((Seg n),X)) by A2; :: thesis: verum