theorem Th33: :: COMPUT_1:34

for i, n being Element of NAT holds arity (n succ i) = n