theorem Th79: :: COMPUT_1:80

for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & arity f1 = 0 holds
(primrec (f1,f2,1)) . <*0*> = f1 . {}