theorem poly2: :: RING_4:10

for L being non empty right_complementable add-associative right_zeroed right_unital distributive associative commutative doubleLoopStr
for p, q being sequence of L
for a being Element of L holds a * (p *' q) = p *' (a * q)