A1: g in PrimRec by Def19;
A2: arity f = 0 by Def24;
f is Element of PrimRec by Def19;
then dom f = 0 -tuples_on NAT by A2, Th25
.= {(<*> NAT )} by FINSEQ_2:112 ;
then A3: {} in dom f by TARSKI:def 1;
A4: f in PrimRec by Def19;
A5: 1 <= 0 + 1 ;
arity g = 0 + 2 by Def26;
hence primrec f,g,1 in PrimRec by A5, A2, A4, A1, Th77; :: according to COMPUT_1:def 19 :: thesis: primrec f,g,1 is unary
reconsider ii = <*0 *> as Element of 1 -tuples_on NAT by FINSEQ_2:151;
dom <*0 *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A6: 1 in dom <*0 *> by TARSKI:def 1;
Del <*0 *>,1 = {} by WSIERP_1:26;
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:97;
len <*0 *> = 1 by FINSEQ_1:56;
hence arity (primrec f,g,1) = 1 by A7, MARGREL1:def 26; :: according to COMPUT_1:def 25 :: thesis: verum