theorem Th24: :: EC_PF_1:24

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