theorem Th69: :: COMPUT_1:70

for i, n being Nat
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) st 1 <= i & i <= n holds
n succ i in P