:: deftheorem Def11 defines primrec COMPUT_1:def 11 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for b₄ being Element of HFuncs NAT holds
( b₄ = primrec (f1,f2,i) iff ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( b₄ = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) );