for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z