theorem Th4: :: INTEGRA7:4

for X being set
for f being PartFunc of REAL,REAL
for x being Real st x in X & f | X is_differentiable_in x holds
f is_differentiable_in x