thus 0 const 0 in majorizedBy AckermannFunction by Th44; :: according to COMPUT_1:def 14 :: thesis: ( 1 succ 1 in majorizedBy AckermannFunction & ( for b₁, b₂ being set holds
( not 1 <= b₂ or not b₂ <= b₁ or b₁ proj b₂ in majorizedBy AckermannFunction ) ) & majorizedBy AckermannFunction is composition_closed & majorizedBy AckermannFunction is primitive-recursion_closed )
thus 1 succ 1 in majorizedBy AckermannFunction by Th50; :: thesis: ( ( for b₁, b₂ being set holds
( not 1 <= b₂ or not b₂ <= b₁ or b₁ proj b₂ in majorizedBy AckermannFunction ) ) & majorizedBy AckermannFunction is composition_closed & majorizedBy AckermannFunction is primitive-recursion_closed )
thus for n, i being Nat st 1 <= i & i <= n holds
n proj i in majorizedBy AckermannFunction by Th52; :: thesis: ( majorizedBy AckermannFunction is composition_closed & majorizedBy AckermannFunction is primitive-recursion_closed )
thus ( majorizedBy AckermannFunction is composition_closed & majorizedBy AckermannFunction is primitive-recursion_closed ) ; :: thesis: verum