reconsider f' = f, fgh = f * <:<*g,h*>:>, g' = g, h' = h as Element of PrimRec by Def19;
rng <*g',h'*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g,h*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider F = <*g,h*> as with_the_same_arity FinSequence of HFuncs NAT by FINSEQ_1:def 4;
A1: ( arity f = 2 & arity g = 2 & arity h = 2 ) by Def26;
then A2: ( dom f' = 2 -tuples_on NAT & dom g' = 2 -tuples_on NAT & dom h' = 2 -tuples_on NAT ) by Lm1;
consider x being Element of 2 -tuples_on NAT ;
A3: dom <:F:> = (dom g) /\ (dom h) by FUNCT_6:62;
( <:F:> . x = <*(g' . x),(h' . x)*> & g' . x in NAT & h' . x in NAT ) by A3, A2, FUNCT_6:62;
then <:F:> . x is Element of 2 -tuples_on NAT by FINSEQ_2:121;
then A4: ( not fgh is empty & f' = f ) by A2, A3, FUNCT_1:21, RELAT_1:60;
rng F = {g,h} by FINSEQ_2:147;
then g in rng F by TARSKI:def 2;
then arity F = 2 by A1, Def7;
hence arity (f * <:<*g,h*>:>) = 2 by A4, Th48; :: according to COMPUT_1:def 26 :: thesis: verum