( dom b = n & rng b c= NAT ) by PARTFUN1:def 2, VALUED_0:def 6;
then reconsider f = b as finite-support Function of n,NAT by RELSET_1:4;
reconsider S = NatMinor f as non empty finite Subset of (Bags n) by Th60;
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 ) assume p divides b ; :: thesis: p in S
then for x being set st x in n holds
p . x <= b . x ;
hence p in S by Def14; :: thesis: verum