theorem Th5: :: FDIFF_12:5

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f is_left_differentiable_in x & x in I & x <> inf I holds
f | I is_left_differentiable_in x