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