theorem Th55: :: COMPUT_1:56

for i being Nat
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function holds dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT