theorem :: COMPUT_1:59

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