for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( f is_differentiable_on 1,Z iff ( Z c= dom f & f | Z is_differentiable_on Z ) )