theorem Th78: :: COMPUT_1:79

for i being Nat
for f1 being NAT * -defined to-naturals homogeneous len-total 1 -ary Function
for f2 being non empty NAT * -defined to-naturals homogeneous Function holds (primrec (f1,f2,2)) . <*i,0*> = f1 . <*i*>