theorem Th10: :: POLYALG1:10

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