reconsider g9 = g, h9 = h as Element of PrimRec by Def16;
A1: f in PrimRec by Def16;
A2: rng <*g9,h9*> 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;
A3: PrimRec is composition_closed by Def14;
A4: arity f = 2 by Def21;
len F = 2 by FINSEQ_1:44;
hence f * <:<*g,h*>:> in PrimRec by A2, A1, A3, A4; :: according to COMPUT_1:def 16 :: thesis: verum