A1: 3 proj 3 in PrimRec by Def14;
A2: 2 -tuples_on PrimRec c= PrimRec * by FINSEQ_2:142;
3 proj 1 in PrimRec by Def14;
then <*(3 proj 1),(3 proj 3)*> in 2 -tuples_on PrimRec by A1, FINSEQ_2:101;
then reconsider F = <*(3 proj 1),(3 proj 3)*> as Element of PrimRec * by A2;
F is with_the_same_arity

proof

let f, g be Function; :: according to COMPUT_1:def 3 :: thesis: ( f in rng F & g in rng F implies ( ( not f is empty or g is empty or dom g = {{}} ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) )
assume that
A3: f in rng F and
A4: g in rng F ; :: thesis: ( ( not f is empty or g is empty or dom g = {{}} ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) )
A5: rng F = {(3 proj 1),(3 proj 3)} by FINSEQ_2:127;
hence ( not f is empty or g is empty or dom g = {{}} ) by A3, TARSKI:def 2; :: thesis: ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) )
assume that
not f is empty and
not g is empty ; :: thesis: ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X )
take 3 ; :: thesis: ex X being non empty set st
( dom f c= 3 -tuples_on X & dom g c= 3 -tuples_on X )
take NAT ; :: thesis: ( dom f c= 3 -tuples_on NAT & dom g c= 3 -tuples_on NAT )
( f = 3 proj 1 or f = 3 proj 3 ) by A3, A5, TARSKI:def 2;
hence dom f c= 3 -tuples_on NAT by Th35; :: thesis: dom g c= 3 -tuples_on NAT
( g = 3 proj 1 or g = 3 proj 3 ) by A4, A5, TARSKI:def 2;
hence dom g c= 3 -tuples_on NAT by Th35; :: thesis: verum

end;

then reconsider F = F as with_the_same_arity Element of PrimRec * ;
let g be primitive-recursive 2 -ary Function; :: thesis: (1,2)->(1,?,2) g in PrimRec
arity g = 2 by Def21;
then A6: arity g = len F by FINSEQ_1:44;
g is Element of PrimRec by Def16;
hence (1,2)->(1,?,2) g in PrimRec by A6, Th71; :: thesis: verum