theorem Th4: :: INTEGR26:4

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_right_convergent_in a holds
( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) )