A1: g in PrimRec by Def16;
A2: arity f = 0 by Def21;
f is Element of PrimRec by Def16;
then dom f = 0 -tuples_on NAT by A2, Th21
.= {(<*> NAT)} by FINSEQ_2:94 ;
then A3: {} in dom f by TARSKI:def 1;
A4: f in PrimRec by Def16;
A5: 1 <= 0 + 1 ;
arity g = 0 + 2 by Def21;
hence primrec (f,g,1) in PrimRec by A5, A2, A4, A1, Th72; :: according to COMPUT_1:def 16 :: thesis: primrec (f,g,1) is 1 -ary
reconsider ii = <*0*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
dom <*0*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A6: 1 in dom <*0*> by TARSKI:def 1;
Del (<*0*>,1) = {} by WSIERP_1:19;
then ii +* (1,0) in dom (primrec (f,g,1)) by A5, A2, A3, A6, Lm6;
then A7: <*0*> in dom (primrec (f,g,1)) by FUNCT_7:95;
len <*0*> = 1 by FINSEQ_1:39;
hence arity (primrec (f,g,1)) = 1 by A7, MARGREL1:def 25; :: according to COMPUT_1:def 21 :: thesis: verum