A1: g in PrimRec by Def19;
A2: 1 <= 1 + 1 ;
A3: arity g = 1 + 2 by Def27;
A4: arity f = 1 by Def25;
f in PrimRec by Def19;
hence primrec f,g,1 in PrimRec by A2, A4, A3, A1, Th77; :: according to COMPUT_1:def 19 :: thesis: primrec f,g,1 is binary
thus arity (primrec f,g,1) = 2 by A2, A4, A3, Th61; :: according to COMPUT_1:def 26 :: thesis: verum