let i be Element of NAT ; :: thesis: for f1 being NAT * -defined to-naturals homogeneous len-total unary 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 unary 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 Def25;
then reconsider p = <*i,0 *> as Element of ((arity f1) + 1) -tuples_on NAT by FINSEQ_2:121;
A1: p +* 2,0 = p by Th3;
( 1 <= 2 & len p = 2 ) by FINSEQ_1:61;
then 2 in dom p by FINSEQ_3:27;
hence (primrec f1,f2,2) . <*i,0 *> = f1 . (Del p,2) by A1, Th64
.= f1 . <*i*> by WSIERP_1:26 ;
:: thesis: verum