theorem Th11: :: POLYNOM1:11

for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)