dom2tuple AckermannFunction is Element of HFuncs NAT by COMPUT_1:28;
hence dom2tuple AckermannFunction in HFuncs NAT ; :: thesis: verum