let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: ( f1 is len-total & arity f1 = 0 implies (primrec f1,f2,1) . <*0 *> = f1 . {} )
assume that
A1: f1 is len-total and
A2: arity f1 = 0 ; :: thesis: (primrec f1,f2,1) . <*0 *> = f1 . {}
reconsider p = <*0 *> as Element of ((arity f1) + 1) -tuples_on NAT by A2;
A3: p +* 1,0 = p by FUNCT_7:97;
( 1 <= 1 & len p = 1 ) by FINSEQ_1:56;
then 1 in dom p by FINSEQ_3:27;
hence (primrec f1,f2,1) . <*0 *> = f1 . (Del p,1) by A1, A3, Th64
.= f1 . {} by WSIERP_1:26 ;
:: thesis: verum