set x = the Element of 2 -tuples_on NAT;
reconsider f9 = f, fg = f * <:<*g*>:>, g9 = g as Element of PrimRec by Def16;
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 FINSEQ_3:141;
arity f = 1
by Def21;
then A3:
dom f9 = 1 -tuples_on NAT
by Lm1;
A4:
arity g = 2
by Def21;
rng F = {g}
by FINSEQ_1:39;
then
g in rng F
by TARSKI:def 1;
then A5:
arity F = 2
by A4, Def4;
A6:
dom g9 = 2 -tuples_on NAT
by A4, Lm1;
then
<:F:> . the Element of 2 -tuples_on NAT = <*(g9 . the Element of 2 -tuples_on NAT)*>
by FINSEQ_3:141;
then
<:F:> . the Element of 2 -tuples_on NAT in 1 -tuples_on NAT
by FINSEQ_2:98;
then
not fg is empty
by A6, A2, A3, FUNCT_1:11, RELAT_1:38;
hence
arity (f * <:<*g*>:>) = 2
by A1, A5, Th43; COMPUT_1:def 21 verum