theorem Th14: :: PDLAX:10

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x being Real st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )