theorem :: COMPUT_1:62

for i, m 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,(m + 1)) in dom (primrec (f1,f2,i)) holds
(primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) by Lm6;