theorem :: ACKERMAN:2

for m being Nat holds m |^|^ 2 = m |^ m by Lm5;