for K being non empty multMagma
for f, g being FinSequence of K
for a being Element of K holds a * (f ^ g) = (a * f) ^ (a * g)