reconsider g9 = g as Element of PrimRec by Def19;
A1: f in PrimRec by Def19;
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 Def17;
A4: arity f = 1 by Def25;
len F = 1 by FINSEQ_1:56;
hence f * <:<*g*>:> in PrimRec by A2, A1, A3, A4, Def15; :: according to COMPUT_1:def 19 :: thesis: verum