set f = dom2tuple AckermannFunction;
assume dom2tuple AckermannFunction is primitive-recursive ; :: thesis: contradiction
then dom2tuple AckermannFunction in PrimRec by COMPUT_1:def 16;
then dom2tuple AckermannFunction in majorizedBy AckermannFunction by Th53;
then ex g being NAT * -defined to-naturals homogeneous Function st
( g = dom2tuple AckermannFunction & AckermannFunction majorizes g ) ;
hence contradiction by Th40; :: thesis: verum