theorem Th19: :: POLYNOM9:19

for n being Nat
for b being bag of n
for i being Nat st b . i = degree b holds
b = (EmptyBag n) +* (i,(b . i))