theorem Th49: :: COMPUT_1:50

for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT st not i in dom p holds
primrec (e1,e2,i,p) = {}