let m, n be Nat; :: thesis: ( 1 <= n & n <= m implies m proj n in majorizedBy AckermannFunction )
assume ( 1 <= n & n <= m ) ; :: thesis: m proj n in majorizedBy AckermannFunction
then AckermannFunction majorizes m proj n by Th51;
hence m proj n in majorizedBy AckermannFunction ; :: thesis: verum