theorem Th5: :: INTEGR26:5

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f | ].a,b.] is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_left_convergent_in b holds
( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) )