set f = H₂(m);
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in rng (AckermannFunction m) or not r <= 0 )
assume r in rng H₂(m) ; :: thesis: not r <= 0
then consider x being object such that
A1: x in dom H₂(m) and
A2: H₂(m) . x = r by FUNCT_1:def 3;
reconsider x = x as Nat by A1;
H₂(m) . x = H₁(m,x) by Def3;
hence not r <= 0 by A2; :: thesis: verum