theorem Th10: :: FDIFF_12:10

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f | I is_left_differentiable_in x holds
( f is_left_differentiable_in x & Ldiff ((f | I),x) = Ldiff (f,x) )