let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function st e1 is empty holds
primrec e1,e2,i is empty
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: ( e1 is empty implies primrec e1,e2,i is empty )
set f1 = e1;
set f2 = e2;
assume A1: e1 is empty ; :: thesis: primrec e1,e2,i is empty
consider G being Function of (((arity e1) + 1) -tuples_on NAT ),(HFuncs NAT ) such that
A2: primrec e1,e2,i = Union G and
A3: for p being Element of ((arity e1) + 1) -tuples_on NAT holds G . p = primrec e1,e2,i,p by Def14;
A4: dom G = ((arity e1) + 1) -tuples_on NAT by FUNCT_2:def 1;

now

let y be set ; :: thesis: ( ( y in rng G implies y in {{} } ) & ( y in {{} } implies y in rng G ) )

hereby :: thesis: ( y in {{} } implies y in rng G )

assume y in rng G ; :: thesis: y in {{} }
then consider x being set such that
A5: ( x in dom G & G . x = y ) by FUNCT_1:def 5;
reconsider p = x as Element of ((arity e1) + 1) -tuples_on NAT by A5;
G . p = primrec e1,e2,i,p by A3
.= {} by A1, Th57 ;
hence y in {{} } by A5, TARSKI:def 1; :: thesis: verum

end;

assume y in {{} } ; :: thesis: y in rng G
then A6: y = {} by TARSKI:def 1;
consider p being Element of ((arity e1) + 1) -tuples_on NAT ;
G . p = primrec e1,e2,i,p by A3
.= {} by A1, Th57 ;
hence y in rng G by A4, A6, FUNCT_1:12; :: thesis: verum

end;

then A7: rng G = {{} } by TARSKI:2;
Union G = union (rng G) by CARD_3:def 4
.= {} by A7, ZFMISC_1:31 ;
hence primrec e1,e2,i is empty by A2; :: thesis: verum