theorem LMDIFF: :: NDIFF_9:1

for E, F being RealNormSpace
for f being PartFunc of E,F
for Z being Subset of E
for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds
( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )