let i, m 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 f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
(primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>)
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 f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
(primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>)
let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: ( f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) )
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: (arity f1) + 2 = arity f2 and
A4: 1 <= i and
A5: i <= 1 + (arity f1) ; :: thesis: (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>)
len p = (arity f1) + 1 by FINSEQ_1:def 18;
then A6: i in dom p by A4, A5, FINSEQ_3:27;
p +* i,(m + 1) in ((arity f1) + 1) -tuples_on NAT ;
then p +* i,(m + 1) in dom (primrec f1,f2,i) by A1, A2, A3, A4, A5, Th61;
hence (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) by A6, Lm6; :: thesis: verum