theorem :: COMPUT_1:58

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 holds
( p +* (i,0) in dom (primrec (f1,f2,i)) iff Del (p,i) in dom f1 ) by Lm6;