theorem Th26: :: POLYNOM1:26

for n being Ordinal
for L being non empty right_complementable distributive Abelian add-associative right_zeroed associative doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)