( dom b = n & rng b c= NAT ) by PARTFUN1:def 4, VALUED_0:def 6;
then reconsider f = b as finite-support Function of n,NAT by RELSET_1:11;
reconsider S = NatMinor f as non empty finite Subset of (Bags n) by Th66;
take IT = SgmX (BagOrder n),S; :: thesis: ex S being non empty finite Subset of (Bags n) st
( IT = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) )
take S ; :: thesis: ( IT = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) )
thus IT = SgmX (BagOrder n),S ; :: thesis: for p being bag of n holds
( p in S iff p divides b )
let p be bag of n; :: thesis: ( p in S iff p divides b )
thus ( p in S implies p divides b ) :: thesis: ( p divides b implies p in S )

proof

assume p in S ; :: thesis: p divides b
then for x being set st x in n holds
p . x <= b . x by Def17;
hence p divides b by Th50; :: thesis: verum

end;

assume p divides b ; :: thesis: p in S
then for x being set st x in n holds
p . x <= b . x by Def13;
hence p in S by Def17; :: thesis: verum