theorem Th56: :: COMPUT_1:57

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