theorem Th36: :: ACKERMAN:36

for m, n being Nat holds (AckermannSequence . m) . <*n*> = Ackermann (m,n)