theorem :: ACKERMAN:28

for m being Nat holds (AckermannFunction (m + 1)) . 0 = (AckermannFunction m) . 1