thus rng AckermannSequence c= HFuncs NAT :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng AckermannSequence or y in HFuncs NAT )
assume y in rng AckermannSequence ; :: thesis: y in HFuncs NAT
then consider x being object such that
A1: x in dom AckermannSequence and
A2: AckermannSequence . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A1;

per cases ( x = 0 or ex n being Nat st x = n + 1 ) by NAT_1:6;

suppose x = 0 ; :: thesis: y in HFuncs NAT

then AckermannSequence . x = 1 succ 1 by Def13;
hence y in HFuncs NAT by A2, COMPUT_1:33; :: thesis: verum

end;

suppose ex n being Nat st x = n + 1 ; :: thesis: y in HFuncs NAT

then consider n being Nat such that
A3: x = n + 1 ;
AckermannSequence . (n + 1) = primrec ((0 const H₁(n,1)),((AckermannSequence . n) * <:<*(2 proj 2)*>:>),1) by Def13;
hence y in HFuncs NAT by A2, A3; :: thesis: verum

end;

end;

end;