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