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