theorem Th1: :: ACKERMAN:1

for m, n being Nat holds m |^|^ (n + 1) = m |^ (m |^|^ n)