reconsider f' = f, fg = f * <:<*g*>:>, g' = g as Element of PrimRec by Def19;
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;
A1: ( arity f = 1 & arity g = 2 ) by Def25, Def26;
then A2: ( dom f' = 1 -tuples_on NAT & dom g' = 2 -tuples_on NAT ) by Lm1;
consider x being Element of 2 -tuples_on NAT ;
A3: dom <:F:> = dom g by FUNCT_6:61;
( <:F:> . x = <*(g' . x)*> & g' . x in NAT ) by A2, FUNCT_6:61;
then A4: ( not fg is empty & f' = f ) by A2, A3, FUNCT_1:21, RELAT_1:60;
rng F = {g} by FINSEQ_1:56;
then g in rng F by TARSKI:def 1;
then arity F = 2 by A1, Def7;
hence arity (f * <:<*g*>:>) = 2 by A4, Th48; :: according to COMPUT_1:def 26 :: thesis: verum