theorem Th1: :: POLYNOM2:1

for L being non empty unital associative multMagma
for a being Element of L
for n, m being Element of NAT holds (power L) . (a,(n + m)) = ((power L) . (a,n)) * ((power L) . (a,m))