let i be 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 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)))*>) ) ) ) ) ;

A4: now :: thesis: for y being Element of n -tuples_on NAT
for k being Nat holds S₂[k]

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

end;

assume g <> {} ; :: thesis: contradiction
then consider x being object 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:35;
hence contradiction by A4, A8; :: thesis: verum