A1: ( 0 <= 1 & 1 <= 0 + 1 & arity f = 0 & arity g = 0 + 2 & f in PrimRec & g in PrimRec ) by Def19, Def24, Def26;
hence primrec f,g,1 in PrimRec by Th77; :: according to COMPUT_1:def 19 :: thesis: primrec f,g,1 is unary
A2: dom <*0 *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
f is Element of PrimRec by Def19;
then dom f = 0 -tuples_on NAT by A1, Th25
.= {(<*> NAT )} by FINSEQ_2:112 ;
then ( Del <*0 *>,1 = {} & {} in dom f & 1 in dom <*0 *> ) by A2, TARSKI:def 1, WSIERP_1:26;
then <*0 *> +* 1,0 in dom (primrec f,g,1) by A1, Lm6;
then ( <*0 *> in dom (primrec f,g,1) & len <*0 *> = 1 ) by FINSEQ_1:56, FUNCT_7:97;
hence arity (primrec f,g,1) = 1 by UNIALG_1:def 10; :: according to COMPUT_1:def 25 :: thesis: verum