reconsider g' = g, h' = h as Element of PrimRec by Def19;
A1: rng <*g',h'*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g,h*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider F = <*g,h*> as with_the_same_arity FinSequence of HFuncs NAT by FINSEQ_1:def 4;
A2: ( f in PrimRec & PrimRec is composition_closed ) by Def17, Def19;
then ( f in HFuncs NAT & len F = 2 & arity f = 2 ) by Def26, FINSEQ_1:61;
hence f * <:<*g,h*>:> in PrimRec by A1, A2, Def15; :: according to COMPUT_1:def 19 :: thesis: verum