theorem Th10: :: POLYNOM1:10

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