theorem Th12: :: CKSPACE1:12

for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )