for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z holds
(#Z n) ^ is_differentiable_on Z