let i be 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:105;
len p = (arity f1) + 1 by CARD_1:def 7;
then len (Del (p,i)) = arity f1 by A1, FINSEQ_3:109;
then A4: Del (p,i) is Element of (arity f1) -tuples_on NAT by A3, FINSEQ_2:92;
dom f1 = (arity f1) -tuples_on NAT by A2, Th22;
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