thus arity (2 succ i) = 2 by Th38; :: according to COMPUT_1:def 26 :: thesis: verum