theorem Th28: :: POLYNOM7:28

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