n in NAT by ORDINAL1:def 12;
then #Z n is_differentiable_on REAL by HFDIFF_1:8;
hence #Z n is differentiable by FUNCT_2:def 1; :: thesis: verum