reconsider g = g, h = h as Element of PrimRec by Def16;
A1:
rng <*g,h*> = {g,h}
by FINSEQ_2:127;
A2:
now for f1, f2 being homogeneous Function st f1 in rng <*g,h*> & f2 in rng <*g,h*> holds
arity f1 = arity f2let f1,
f2 be
homogeneous Function;
( f1 in rng <*g,h*> & f2 in rng <*g,h*> implies arity f1 = arity f2 )assume that A3:
f1 in rng <*g,h*>
and A4:
f2 in rng <*g,h*>
;
arity f1 = arity f2
(
f1 = g or
f1 = h )
by A1, A3, TARSKI:def 2;
then A5:
arity f1 = 2
by Def21;
(
f2 = g or
f2 = h )
by A1, A4, TARSKI:def 2;
hence
arity f1 = arity f2
by A5, Def21;
verum end;
rng <*g,h*> c= PrimRec
by FINSEQ_1:def 4;
hence
<*g,h*> is with_the_same_arity
by A2, Th29, XBOOLE_1:1; verum