reconsider g' = g as Element of PrimRec by Def19;
A1: rng <*g'*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider F = <*g'*> 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 = 1 & arity f = 1 ) by Def25, FINSEQ_1:56;
hence f * <:<*g*>:> in PrimRec by A1, A2, Def15; :: according to COMPUT_1:def 19 :: thesis: verum