theorem :: POLYRED:13

for n being Ordinal
for b, b9 being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b9 + b) = p . b9 by Lm9;