theorem Th63: :: COMPUT_1:64

for i being Nat
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st (arity f1) + 2 = arity f2 & 1 <= i & i <= (arity f1) + 1 holds
primrec (f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i