reconsider g = g, h = h as Element of PrimRec by Def16;
A1: rng <*g,h*> = {g,h} by FINSEQ_2:127;

A2: now :: thesis: for f1, f2 being homogeneous Function st f1 in rng <*g,h*> & f2 in rng <*g,h*> holds
arity f1 = arity f2

let f1, f2 be homogeneous Function; :: thesis: ( 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*> ; :: thesis: 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; :: thesis: 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; :: thesis: verum