let g be NAT * -defined to-naturals homogeneous Function; :: thesis: ( arity g = 0 implies AckermannFunction majorizes g )
assume A1: arity g = 0 ; :: thesis: AckermannFunction majorizes g
take N = 0 ; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom g holds
for a being Element of NAT st a = max (rng F) holds
g . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom g implies for a being Element of NAT st a = max (rng F) holds
g . F < AckermannFunction . (N,a) )
assume A2: F in dom g ; :: thesis: for a being Element of NAT st a = max (rng F) holds
g . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies g . F < AckermannFunction . (N,a) )
assume a = max (rng F) ; :: thesis: g . F < AckermannFunction . (N,a)
len F = 0 by A1, A2, MARGREL1:def 25;
hence g . F < AckermannFunction . (N,a) ; :: thesis: verum