let i be Element of NAT ; :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2 holds
(primrec (f1,f2,1)) . <*(i + 1)*> = f2 . <*i,((primrec (f1,f2,1)) . <*i*>)*>
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: ( f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2 implies (primrec (f1,f2,1)) . <*(i + 1)*> = f2 . <*i,((primrec (f1,f2,1)) . <*i*>)*> )
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: arity f1 = 0 and
A4: arity f2 = 2 ; :: thesis: (primrec (f1,f2,1)) . <*(i + 1)*> = f2 . <*i,((primrec (f1,f2,1)) . <*i*>)*>
reconsider p = <*i*> as Element of ((arity f1) + 1) -tuples_on NAT by A3, FINSEQ_2:131;
A5: p +* (1,(i + 1)) = <*(i + 1)*> by FUNCT_7:95;
A6: p +* (1,i) = <*i*> by FUNCT_7:95;
(arity f1) + 2 = arity f2 by A3, A4;
hence (primrec (f1,f2,1)) . <*(i + 1)*> = f2 . ((p +* (1,i)) ^ <*((primrec (f1,f2,1)) . (p +* (1,i)))*>) by A1, A2, A3, A5, Th62
.= f2 . <*i,((primrec (f1,f2,1)) . <*i*>)*> by A6, FINSEQ_1:def 9 ;
:: thesis: verum