theorem Th18: :: POLYRED:18

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L
for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)