let i be Element of NAT ; :: thesis: for f1, f2 being non empty to-naturals homogeneous from-natural-fseqs Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & f1 is len-total holds
(primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i)
let f1, f2 be non empty to-naturals homogeneous from-natural-fseqs Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & f1 is len-total holds
(primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i)
let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: ( i in dom p & f1 is len-total implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) )
assume that
A1: i in dom p and
A2: f1 is len-total ; :: thesis: (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i)
len p = (arity f1) + 1 by FINSEQ_2:109;
then A3: len (Del p,i) = arity f1 by A1, FINSEQ_3:118;
A4: dom f1 = (arity f1) -tuples_on NAT by A2, Th26;
Del p,i is FinSequence of NAT by FINSEQ_3:114;
then Del p,i is Element of (arity f1) -tuples_on NAT by A3, FINSEQ_2:110;
then p +* i,0 in dom (primrec f1,f2,i) by A1, A4, Lm6;
hence (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) by A1, Lm6; :: thesis: verum