theorem Th72: :: COMPUT_1:73

for P being non empty primitive-recursively_closed Subset of (HFuncs NAT)
for f1, f2 being Element of P st (arity f1) + 2 = arity f2 holds
for i being Nat st 1 <= i & i <= (arity f1) + 1 holds
primrec (f1,f2,i) in P