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

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:113; :: thesis: verum