theorem Th51: :: COMPUT_1:52

for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT holds dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT