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