for F being RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )