theorem Th81: :: COMPUT_1:82

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