theorem Th30: :: POLYNOM3:32

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