let g1, g2 be Element of HFuncs NAT; :: thesis: ( ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( g1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) & ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( g2 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) implies g1 = g2 )
given G1 being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that A9: g1 = Union G1 and
A10: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G1 . p = primrec (f1,f2,i,p) ; :: thesis: ( for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) holds
( not g2 = Union G or ex p being Element of ((arity f1) + 1) -tuples_on NAT st not G . p = primrec (f1,f2,i,p) ) or g1 = g2 )
given G2 being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that A11: g2 = Union G2 and
A12: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G2 . p = primrec (f1,f2,i,p) ; :: thesis: g1 = g2

now :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G1 . p = G2 . p

let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: G1 . p = G2 . p
thus G1 . p = primrec (f1,f2,i,p) by A10
.= G2 . p by A12 ; :: thesis: verum

end;

hence g1 = g2 by A9, A11, FUNCT_2:63; :: thesis: verum