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 Def11;
A4: dom G = ((arity e1) + 1) -tuples_on NAT by FUNCT_2:def 1;
now :: thesis: for y being object holds
( ( y in rng G implies y in {{}} ) & ( y in {{}} implies y in rng G ) )
set p = the Element of ((arity e1) + 1) -tuples_on NAT;
let y be object ; :: 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 object such that
A5: x in dom G and
A6: G . x = y by FUNCT_1:def 3;
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, Th52 ;
hence y in {{}} by A6, TARSKI:def 1; :: thesis: verum
end;
assume y in {{}} ; :: thesis: y in rng G
then A7: y = {} by TARSKI:def 1;
G . the Element of ((arity e1) + 1) -tuples_on NAT = primrec (e1,e2,i, the Element of ((arity e1) + 1) -tuples_on NAT) by A3
.= {} by A1, Th52 ;
hence y in rng G by A4, A7, FUNCT_1:3; :: thesis: verum
end;
then A8: rng G = {{}} by TARSKI:2;
Union G = union (rng G)
.= {} by A8, ZFMISC_1:25 ;
hence primrec (e1,e2,i) is empty by A2; :: thesis: verum