theorem Th54: :: COMPUT_1:55

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