A5:
g in PrimRec
by Def16;
A6:
2 <= 1 + 1
;
A7:
arity g = 1 + 2
by Def21;
A8:
arity f = 1
by Def21;
f in PrimRec
by Def16;
hence
primrec (f,g,2) in PrimRec
by A6, A8, A7, A5, Th72; COMPUT_1:def 16 primrec (f,g,2) is 2 -ary
thus
arity (primrec (f,g,2)) = 2
by A6, A8, A7, Th56; COMPUT_1:def 21 verum