reconsider g9 = g as Element of PrimRec by Def16;
A1: f in PrimRec by Def16;
A2: rng <*g9*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider F = <*g9*> as with_the_same_arity FinSequence of HFuncs NAT by FINSEQ_1:def 4;
A3: PrimRec is composition_closed by Def14;
A4: arity f = 1 by Def21;
len F = 1 by FINSEQ_1:39;
hence f * <:<*g*>:> in PrimRec by A2, A1, A3, A4; :: according to COMPUT_1:def 16 :: thesis: verum