theorem Th59: :: COMPUT_1:60

for i being Nat
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & f1 is len-total holds
(primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i))