theorem Th30: :: NDIFF_1:30

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S by XBOOLE_1:1;