theorem Th38: :: ACKERMAN:38

for m being Nat holds dom2tuple (AckermannFunction (m + 1)) = primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)