theorem Th20: :: WALLIS01:23

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