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 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 CARD_1:def 7;
then A7: i in dom p by A4, A5, FINSEQ_3:25;
then A8: p /. i = p . i by PARTFUN1:def 6;
consider F being sequence of (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 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 Def10;
defpred S2[ Nat] means p +* (i,$1) in dom (F . $1);
A12: p +* (i,(p . i)) = p by FUNCT_7:35;
A13: now :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be 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 ;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set pc = (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>;
reconsider p2 = <*aa*> as FinSequence of NAT ;
reconsider p1 = (p +* (i,mm)) ^ p2 as FinSequence of NAT ;
A15: len p2 = 1 by CARD_1:def 7;
len (p +* (i,mm)) = 1 + (arity f1) by CARD_1:def 7;
then len p1 = ((arity f1) + 1) + 1 by A15, FINSEQ_1:22
.= arity f2 by A3 ;
then A16: p1 is Element of (arity f2) -tuples_on NAT by FINSEQ_2:92;
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)))*>))) ;
dom f2 = (arity f2) -tuples_on NAT by A2, Th22;
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 :: thesis: S2[ 0 ]
reconsider Dpi = Del (p,i) as FinSequence of NAT by FINSEQ_3:105;
reconsider Dpi9 = Dpi as Element of (len Dpi) -tuples_on NAT by FINSEQ_2:92;
A19: dom f1 = (arity f1) -tuples_on NAT by A1, Th22;
len (Del (p,i)) = arity f1 by A6, A7, FINSEQ_3:109;
then Dpi9 in dom f1 by A19;
then dom (F . 0) = {(p +* (i,0))} by A4, A5, A6, A10, FINSEQ_3:25;
hence S2[ 0 ] by TARSKI:def 1; :: thesis: verum
end;
for m being Nat holds S2[m] from NAT_1:sch 2(A18, A13);
 hence p in dom (primrec (f1,f2,i,p)) by A8, A9, A12; :: thesis: verum