theorem Th27: :: POLYNOM7:27

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | (n,L)) *' p