theorem Th22: :: POLYNOM1:22

for n being set
for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S