let i, j be Element of NAT ; :: thesis: for f1 being NAT * -defined to-naturals homogeneous len-total unary Function
for f2 being NAT * -defined to-naturals homogeneous len-total ternary Function holds (primrec f1,f2,2) . <*i,(j + 1)*> = f2 . <*i,j,((primrec f1,f2,2) . <*i,j*>)*>
let f1 be NAT * -defined to-naturals homogeneous len-total unary Function; :: thesis: for f2 being NAT * -defined to-naturals homogeneous len-total ternary Function holds (primrec f1,f2,2) . <*i,(j + 1)*> = f2 . <*i,j,((primrec f1,f2,2) . <*i,j*>)*>
let f2 be NAT * -defined to-naturals homogeneous len-total ternary Function; :: thesis: (primrec f1,f2,2) . <*i,(j + 1)*> = f2 . <*i,j,((primrec f1,f2,2) . <*i,j*>)*>
A1: arity f1 = 1 by Def25;
then reconsider p = <*i,j*> as Element of ((arity f1) + 1) -tuples_on NAT by FINSEQ_2:121;
A2: p +* 2,(j + 1) = <*i,(j + 1)*> by Th3;
A3: p +* 2,j = <*i,j*> by Th3;
(arity f1) + 2 = arity f2 by A1, Def27;
hence (primrec f1,f2,2) . <*i,(j + 1)*> = f2 . ((p +* 2,j) ^ <*((primrec f1,f2,2) . (p +* 2,j))*>) by A1, A2, Th67
.= f2 . <*i,j,((primrec f1,f2,2) . <*i,j*>)*> by A3, FINSEQ_1:60 ;
:: thesis: verum