for F being RealNormSpace
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z