A5: g in PrimRec by Def19;
A6: 2 <= 1 + 1 ;
A7: arity g = 1 + 2 by Def24;
A8: arity f = 1 by Def24;
f in PrimRec by Def19;
hence primrec (f,g,2) in PrimRec by A6, A8, A7, A5, Th77; :: according to COMPUT_1:def 16 :: thesis: primrec (f,g,2) is 2 -ary
thus arity (primrec (f,g,2)) = 2 by A6, A8, A7, Th61; :: according to COMPUT_1:def 21 :: thesis: verum