theorem Th36: :: INTEGR26:36

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