theorem Th10: :: BINOM:10

for R being non empty unital associative multMagma
for a being Element of R
for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)