theorem Th7: :: ACKERMAN:7

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