let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p being FinSequence of NAT holds dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for p being FinSequence of NAT holds dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT
set f1 = e1;
set f2 = e2;
let p be FinSequence of NAT ; :: thesis: dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT

per cases ( i in dom p or not i in dom p ) ;

suppose A1: i in dom p ; :: thesis: dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT

consider F being Function of NAT ,(HFuncs NAT ) such that
A2: primrec e1,e2,i,p = F . (p /. i) and
A3: ( i in dom p & Del p,i in dom e1 implies F . 0 = (p +* i,0 ) .--> (e1 . (Del p,i)) ) and
A4: ( ( not i in dom p or not Del p,i in dom e1 ) implies F . 0 = {} ) and
A5: for m being Element of NAT holds S₁[m,F . m,F . (m + 1),p,i,e2] by Def13;
defpred S₂[ Element of NAT ] means dom (F . $1) c= (1 + (arity e1)) -tuples_on NAT ;

A6: now

let m be Element of NAT ; :: thesis: ( S₂[m] implies S₂[b₁ + 1] )
assume A7: S₂[m] ; :: thesis: S₂[b₁ + 1]
set pc = (p +* i,m) ^ <*((F . m) . (p +* i,m))*>;

per cases ( ( p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) ;

suppose A8: ( p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) ; :: thesis: S₂[b₁ + 1]

dom (p +* i,m) = dom p by FUNCT_7:32
.= dom (p +* i,(m + 1)) by FUNCT_7:32 ;
then A9: len (p +* i,m) = len (p +* i,(m + 1)) by FINSEQ_3:31;
len (p +* i,m) = 1 + (arity e1) by A7, A8, FINSEQ_1:def 18;
then p +* i,(m + 1) is Element of (1 + (arity e1)) -tuples_on NAT by A9, FINSEQ_2:110;
then A10: {(p +* i,(m + 1))} c= (1 + (arity e1)) -tuples_on NAT by ZFMISC_1:37;
F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (e2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) by A1, A5, A8;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ((p +* i,(m + 1)) .--> (e2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>)))) by FUNCT_4:def 1;
then dom (F . (m + 1)) = (dom (F . m)) \/ {(p +* i,(m + 1))} by FUNCOP_1:19;
hence S₂[m + 1] by A7, A10, XBOOLE_1:8; :: thesis: verum

end;

suppose ( not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) ; :: thesis: S₂[b₁ + 1]

hence S₂[m + 1] by A5, A7; :: thesis: verum

end;

end;

end;

A11: S₂[ 0 ]

proof

per cases ( Del p,i in dom e1 or not Del p,i in dom e1 ) ;

suppose A12: Del p,i in dom e1 ; :: thesis: S₂[ 0 ]

dom e1 c= (arity e1) -tuples_on NAT by Th24;
then A13: len (Del p,i) = arity e1 by A12, FINSEQ_1:def 18;
A14: dom p = dom (p +* i,0 ) by FUNCT_7:32;
p <> <*> NAT by A1;
then consider n being Nat such that
A15: len p = n + 1 by NAT_1:6;
len (Del p,i) = n by A1, A15, FINSEQ_3:118;
then len (p +* i,0 ) = 1 + (arity e1) by A13, A15, A14, FINSEQ_3:31;
then A16: p +* i,0 is Element of (1 + (arity e1)) -tuples_on NAT by FINSEQ_2:110;
dom (F . 0 ) = {(p +* i,0 )} by A1, A3, A12, FUNCOP_1:19;
hence S₂[ 0 ] by A16, ZFMISC_1:37; :: thesis: verum

end;

suppose not Del p,i in dom e1 ; :: thesis: S₂[ 0 ]

hence S₂[ 0 ] by A4, RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

end;

end;

for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A11, A6);
hence dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT by A2; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT

then primrec e1,e2,i,p = {} by Th54;
hence dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT by RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

end;