theorem :: GROUP_1:52

for L being non empty unital associative commutative multMagma
for x, y being Element of L
for n being Nat holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))