theorem Th8: :: HFDIFF_1:8

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