reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;
AckermannFunction . (m,n) is Element of NAT ;
hence AckermannFunction . (m,n) is Element of NAT ; :: thesis: verum