theorem poly3: :: RING_4:11
for L being non empty associative multMagma
for p being sequence of L
for a, b being Element of L holds (a * b) * p = a * (b * p)