theorem Th29: :: POLYNOM3:31

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