:: deftheorem Def1 defines NBag1 POLYALGX:def 1 :
for b₁ being Function of NAT,(Bags 1) holds
( b₁ = NBag1 iff for m being Element of NAT holds b₁ . m = 1 --> m );