:: deftheorem Def2 defines BagN1 POLYALGX:def 2 :
for b₁ being Function of (Bags 1),NAT holds
( b₁ = BagN1 iff for b being Element of Bags 1 holds b₁ . b = b . 0 );