A1: g in PrimRec by Def16;
A2: 1 <= 1 + 1 ;
A3: arity g = 1 + 2 by Def21;
A4: arity f = 1 by Def21;
f in PrimRec by Def16;
hence primrec (f,g,1) in PrimRec by A2, A4, A3, A1, Th72; :: according to COMPUT_1:def 16 :: thesis: primrec (f,g,1) is 2 -ary
thus arity (primrec (f,g,1)) = 2 by A2, A4, A3, Th56; :: according to COMPUT_1:def 21 :: thesis: verum