for n being Element of NAT holds #Z n is_differentiable_on REAL