let e1, e2 be NAT * -defined to-naturals homogeneous Function; for i being Nat
for p being FinSequence of NAT st not i in dom p holds
primrec (e1,e2,i,p) = {}
let i be Nat; for p being FinSequence of NAT st not i in dom p holds
primrec (e1,e2,i,p) = {}
set f1 = e1;
set f2 = e2;
let p be FinSequence of NAT ; ( not i in dom p implies primrec (e1,e2,i,p) = {} )
consider F being sequence of (HFuncs NAT) such that
A1:
primrec (e1,e2,i,p) = F . (p /. i)
and
( i in dom p & Del (p,i) in dom e1 implies F . 0 = (p +* (i,0)) .--> (e1 . (Del (p,i))) )
and
A2:
( ( not i in dom p or not Del (p,i) in dom e1 ) implies F . 0 = {} )
and
A3:
for m being Nat holds S1[m,F . m,F . (m + 1),p,i,e2]
by Def10;
defpred S2[ Nat] means F . $1 = {} ;
assume A4:
not i in dom p
; primrec (e1,e2,i,p) = {}
then A5:
for m being Nat st S2[m] holds
S2[m + 1]
by A3;
A6:
S2[ 0 ]
by A4, A2;
for m being Nat holds S2[m]
from NAT_1:sch 2(A6, A5);
hence
primrec (e1,e2,i,p) = {}
by A1; verum