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