for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p, q being FinSequence of NAT st q in dom (primrec (e1,e2,i,p)) holds
ex k being Element of NAT st q = p +* (i,k)