let i be Element of NAT ; :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous 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 NAT * -defined to-naturals homogeneous 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)
A3: Del p,i is FinSequence of NAT by FINSEQ_3:114;
len p = (arity f1) + 1 by FINSEQ_1:def 18;
then len (Del p,i) = arity f1 by A1, FINSEQ_3:118;
then A4: Del p,i is Element of (arity f1) -tuples_on NAT by A3, FINSEQ_2:110;
dom f1 = (arity f1) -tuples_on NAT by A2, Th26;
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