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 CARD_1:def 7;
then A6: i in dom p by A4, A5, FINSEQ_3:25;
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, Th56;
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