for i being Element of NAT
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p being FinSequence of NAT st e1 is empty holds
primrec (e1,e2,i,p) is empty