let m, n be Nat; :: thesis: ( 1 <= n & n <= m implies AckermannFunction majorizes m proj n )
assume A1: ( 1 <= n & n <= m ) ; :: thesis: AckermannFunction majorizes m proj n
set g = m proj n;
take N = n + 1; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom (m proj n) holds
for a being Element of NAT st a = max (rng F) holds
(m proj n) . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom (m proj n) implies for a being Element of NAT st a = max (rng F) holds
(m proj n) . F < AckermannFunction . (N,a) )
assume A2: F in dom (m proj n) ; :: thesis: for a being Element of NAT st a = max (rng F) holds
(m proj n) . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies (m proj n) . F < AckermannFunction . (N,a) )
assume A3: a = max (rng F) ; :: thesis: (m proj n) . F < AckermannFunction . (N,a)
A4: dom (m proj n) = m -tuples_on NAT by COMPUT_1:36;
then A5: (m proj n) . F = F . n by A2, COMPUT_1:38;
len F = m by A2, A4, FINSEQ_2:132;
then n in dom F by A1, FINSEQ_3:25;
then F . n in rng F by FUNCT_1:def 3;
then A6: F . n <= a by A3, XXREAL_2:def 8;
H₁( 0 ,a) <= H₁(N,a) by Th24;
hence (m proj n) . F < AckermannFunction . (N,a) by A6, A5, Th16, XXREAL_0:2; :: thesis: verum