set x = the Element of 2 -tuples_on NAT;
reconsider f9 = f, fgh = f * <:<*g,h*>:>, g9 = g, h9 = h as Element of PrimRec by Def16;
A1: f9 = f ;
rng <*g9,h9*> 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;
A2: dom <:F:> = (dom g) /\ (dom h) by FINSEQ_3:142;
A3: arity g = 2 by Def21;
rng F = {g,h} by FINSEQ_2:127;
then g in rng F by TARSKI:def 2;
then A4: arity F = 2 by A3, Def4;
arity f = 2 by Def21;
then A5: dom f9 = 2 -tuples_on NAT by Lm1;
arity h = 2 by Def21;
then A6: dom h9 = 2 -tuples_on NAT by Lm1;
A7: dom g9 = 2 -tuples_on NAT by A3, Lm1;
then <:F:> . the Element of 2 -tuples_on NAT = <*(g9 . the Element of 2 -tuples_on NAT),(h9 . the Element of 2 -tuples_on NAT)*> by A6, A2, FINSEQ_3:142;
then <:F:> . the Element of 2 -tuples_on NAT is Element of 2 -tuples_on NAT by FINSEQ_2:101;
then not fgh is empty by A5, A7, A6, A2, FUNCT_1:11, RELAT_1:38;
hence arity (f * <:<*g,h*>:>) = 2 by A1, A4, Th43; :: according to COMPUT_1:def 21 :: thesis: verum