theorem Th6: :: HILB10_2:6

for n being Nat
for b being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b