theorem Th80: :: COMPUT_1:81

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