set n = (arity f1) + 1;
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th31;
deffunc H₁( FinSequence of NAT ) -> Element of HFuncs NAT = primrec f1,f2,i,$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();
consider np being Element of ((arity f1) + 1) -tuples_on NAT ;
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 & f = G . x ) by FUNCT_1:def 5;
assume g in Y ; :: thesis: f tolerates g
then consider y being set such that
A4: ( y in dom G & g = G . y ) by FUNCT_1:def 5;
reconsider x = x, y = y as Element of ((arity f1) + 1) -tuples_on NAT by A3, A4;
( f = primrec ff1,ff2,i,x & g = primrec ff1,ff2,i,y ) by A1, A3, A4;
hence f tolerates g by 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
A5: ( g = Union G & 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, A5; :: thesis: verum