deffunc H₁( FinSequence of NAT ) -> Element of HFuncs NAT = primrec (f1,f2,i,$1);
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th31;
set n = (arity f1) + 1;
consider G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that
A1: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = H₁(p) from FUNCT_2:sch 4();
reconsider Y = rng G as non empty Subset of (HFuncs NAT) by RELAT_1:def 19;
Y is PartFunc-set of NAT * , NAT

proof

let f be Element of Y; :: according to RFUNCT_3:def 3 :: thesis: f is Element of bool [:(NAT *),NAT:]
thus f is Element of bool [:(NAT *),NAT:] ; :: thesis: verum

end;

then reconsider Y = Y as PFUNC_DOMAIN of NAT * , NAT ;
A2: Y is compatible

proof

let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in Y & g in Y implies f tolerates g )
assume f in Y ; :: thesis: ( not g in Y or f tolerates g )
then consider x being set such that
A3: x in dom G and
A4: f = G . x by FUNCT_1:def 3;
assume g in Y ; :: thesis: f tolerates g
then consider y being set such that
A5: y in dom G and
A6: g = G . y by FUNCT_1:def 3;
reconsider x = x, y = y as Element of ((arity f1) + 1) -tuples_on NAT by A3, A5;
A7: g = primrec (ff1,ff2,i,y) by A1, A6;
f = primrec (ff1,ff2,i,x) by A1, A4;
hence f tolerates g by A7, Th55; :: thesis: verum

end;

now

let x be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: dom (G . x) c= ((arity f1) + 1) -tuples_on NAT
G . x = primrec (ff1,ff2,i,x) by A1;
hence dom (G . x) c= ((arity f1) + 1) -tuples_on NAT by Th56; :: thesis: verum

end;

then consider g being Element of HFuncs NAT such that
A8: g = Union G and
dom g c= ((arity f1) + 1) -tuples_on NAT by A2, Th43;
take g ; :: thesis: ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
take G ; :: thesis: ( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
thus ( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) by A1, A8; :: thesis: verum