theorem Th33: :: COMPUT_1:34
for i, n being Nat holds arity (n succ i) = n