theorem Th22: :: POLYRED:22

for n being Ordinal
for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p