let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function
for g being Element of HFuncs NAT st e1 = {} & g is_primitive-recursively_expressed_by e1,e2,i holds
g = {}
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for g being Element of HFuncs NAT st e1 = {} & g is_primitive-recursively_expressed_by e1,e2,i holds
g = {}
set f1 = e1;
set f2 = e2;
let g be Element of HFuncs NAT ; :: thesis: ( e1 = {} & g is_primitive-recursively_expressed_by e1,e2,i implies g = {} )
assume A1: e1 = {} ; :: thesis: ( not g is_primitive-recursively_expressed_by e1,e2,i or g = {} )
assume g is_primitive-recursively_expressed_by e1,e2,i ; :: thesis: g = {}
then consider n being Element of NAT such that
A2: dom g c= n -tuples_on NAT and
i >= 1 and
i <= n and
(arity e1) + 1 = n and
n + 1 = arity e2 and
A3: for p being FinSequence of NAT st len p = n holds
( ( p +* i,0 in dom g implies Del p,i in dom e1 ) & ( Del p,i in dom e1 implies p +* i,0 in dom g ) & ( p +* i,0 in dom g implies g . (p +* i,0 ) = e1 . (Del p,i) ) & ( for n being Element of NAT holds
( ( p +* i,(n + 1) in dom g implies ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom e2 ) ) & ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom e2 implies p +* i,(n + 1) in dom g ) & ( p +* i,(n + 1) in dom g implies g . (p +* i,(n + 1)) = e2 . ((p +* i,n) ^ <*(g . (p +* i,n))*>) ) ) ) ) by Def12;

A4: now

let y be Element of n -tuples_on NAT ; :: thesis: for k being Element of NAT holds S₂[k]
defpred S₂[ Element of NAT ] means not y +* i,$1 in dom g;
A5: len y = n by FINSEQ_1:def 18;
then A6: for k being Element of NAT st S₂[k] holds
S₂[k + 1] by A3;
A7: S₂[ 0 ] by A1, A3, A5;
thus for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A7, A6); :: thesis: verum

end;

assume g <> {} ; :: thesis: contradiction
then consider x being set such that
A8: x in dom g by XBOOLE_0:def 1;
reconsider x = x as Element of n -tuples_on NAT by A2, A8;
set xi = x . i;
x = x +* i,(x . i) by FUNCT_7:37;
hence contradiction by A4, A8; :: thesis: verum