let i, j be Nat; :: thesis: 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*>)*>
let f1 be NAT * -defined to-naturals homogeneous len-total 1 -ary Function; :: thesis: 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*>)*>
let f2 be NAT * -defined to-naturals homogeneous len-total 3 -ary Function; :: thesis: (primrec (f1,f2,2)) . <*i,(j + 1)*> = f2 . <*i,j,((primrec (f1,f2,2)) . <*i,j*>)*>
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
A1: arity f1 = 1 by Def21;
then reconsider p = <*i1,j1*> as Element of ((arity f1) + 1) -tuples_on NAT by FINSEQ_2:101;
A2: p +* (2,(j + 1)) = <*i,(j + 1)*> by Th1;
A3: p +* (2,j) = <*i,j*> by Th1;
(arity f1) + 2 = arity f2 by A1, Def21;
hence (primrec (f1,f2,2)) . <*i,(j + 1)*> = f2 . ((p +* (2,j)) ^ <*((primrec (f1,f2,2)) . (p +* (2,j)))*>) by A1, A2, Th62
.= f2 . <*i,j,((primrec (f1,f2,2)) . <*i,j*>)*> by A3, FINSEQ_1:43 ;
:: thesis: verum