let i be Element of NAT ; :: thesis: 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*>
let f1 be NAT * -defined to-naturals homogeneous len-total 1 -ary Function; :: thesis: for f2 being non empty NAT * -defined to-naturals homogeneous Function holds (primrec (f1,f2,2)) . <*i,0*> = f1 . <*i*>
let f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: (primrec (f1,f2,2)) . <*i,0*> = f1 . <*i*>
arity f1 = 1 by Def21;
then reconsider p = <*i,0*> as Element of ((arity f1) + 1) -tuples_on NAT by FINSEQ_2:101;
len p = 2 by FINSEQ_1:44;
then A1: 2 in dom p by FINSEQ_3:25;
p +* (2,0) = p by Th1;
hence (primrec (f1,f2,2)) . <*i,0*> = f1 . (Del (p,2)) by A1, Th59
.= f1 . <*i*> by WSIERP_1:19 ;
:: thesis: verum