theorem Th12: :: POLYRED:12

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