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 f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
p in dom (primrec f1,f2,i,p)
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
p in dom (primrec f1,f2,i,p)
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 p in dom (primrec f1,f2,i,p) )
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: p in dom (primrec f1,f2,i,p)
A6: len p = 1 + (arity f1) by FINSEQ_1:def 18;
then A7: i in dom p by A4, A5, FINSEQ_3:27;
then A8: p /. i = p . i by PARTFUN1:def 8;
consider F being Function of NAT ,(HFuncs NAT ) such that
A9: primrec f1,f2,i,p = F . (p /. i) and
A10: ( i in dom p & Del p,i in dom f1 implies F . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) and
( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) and
A11: for m being Element of NAT holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) by Def13;
defpred S2[ Element of NAT ] means p +* i,$1 in dom (F . $1);
A12: p +* i,(p . i) = p by FUNCT_7:37;
A13: now
let m be Element of NAT ; :: thesis: ( S2[m] implies S2[m + 1] )
assume A14: S2[m] ; :: thesis: S2[m + 1]
reconsider aa = (F . m) . (p +* i,m) as Element of NAT ;
set pc = (p +* i,m) ^ <*((F . m) . (p +* i,m))*>;
reconsider p2 = <*aa*> as FinSequence of NAT ;
reconsider p1 = (p +* i,m) ^ p2 as FinSequence of NAT ;
A15: len p2 = 1 by FINSEQ_1:def 18;
len (p +* i,m) = 1 + (arity f1) by FINSEQ_1:def 18;
then len p1 = ((arity f1) + 1) + 1 by A15, FINSEQ_1:35
.= arity f2 by A3 ;
then A16: p1 is Element of (arity f2) -tuples_on NAT by FINSEQ_2:110;
p +* i,(m + 1) in {(p +* i,(m + 1))} by TARSKI:def 1;
then A17: p +* i,(m + 1) in dom ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) by FUNCOP_1:19;
dom f2 = (arity f2) -tuples_on NAT by A2, Th26;
then F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) by A7, A11, A14, A16;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>)))) by FUNCT_4:def 1;
hence S2[m + 1] by A17, XBOOLE_0:def 3; :: thesis: verum
end;
A18: now
reconsider Dpi = Del p,i as FinSequence of NAT by FINSEQ_3:114;
reconsider Dpi9 = Dpi as Element of (len Dpi) -tuples_on NAT by FINSEQ_2:110;
A19: dom f1 = (arity f1) -tuples_on NAT by A1, Th26;
len (Del p,i) = arity f1 by A6, A7, FINSEQ_3:118;
then Dpi9 in dom f1 by A19;
then dom (F . 0 ) = {(p +* i,0 )} by A4, A5, A6, A10, FINSEQ_3:27, FUNCOP_1:19;
hence S2[ 0 ] by TARSKI:def 1; :: thesis: verum
end;
for m being Element of NAT holds S2[m] from NAT_1:sch 1(A18, A13);
 hence p in dom (primrec f1,f2,i,p) by A8, A9, A12; :: thesis: verum