let a, b be 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) )
let f, F be PartFunc of REAL,REAL; ( 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) ) implies ( F is_left_differentiable_in b & Ldiff (F,b) = lim_left ((F `| ].a,b.[),b) ) )
assume that
A1:
a < b
and
A2:
[.a,b.] c= dom f
and
A3:
f | [.a,b.] is continuous
and
A4:
[.a,b.] c= dom F
and
A5:
for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x)
; ( F is_left_differentiable_in b & Ldiff (F,b) = lim_left ((F `| ].a,b.[),b) )
A6:
[.a,b.] = ['a,b']
by A1, INTEGRA5:def 3;
].a,b.[ c= [.a,b.]
by XXREAL_1:25;
then A7:
( ].a,b.[ c= dom f & ].a,b.[ c= dom F )
by A2, A4;
A8:
].a,b.] c= [.a,b.]
by XXREAL_1:23;
then A9:
].a,b.] c= dom F
by A4;
for x being Real st x in ].a,b.[ holds
F | ].a,b.[ is_differentiable_in x
proof
let x be
Real;
( x in ].a,b.[ implies F | ].a,b.[ is_differentiable_in x )
assume A10:
x in ].a,b.[
;
F | ].a,b.[ is_differentiable_in x
then
F is_differentiable_in x
by A1, A2, A3, A4, A5, Th32;
hence
F | ].a,b.[ is_differentiable_in x
by A10, PDIFFEQ1:2;
verum
end;
then A11:
F is_differentiable_on ].a,b.[
by A7;
A12:
F `| ].a,b.[ is_left_convergent_in b
by A1, A2, A3, A4, A5, Th34;
A13:
dom (F | [.a,b.]) = [.a,b.]
by A4, RELAT_1:62;
A14:
for x being Real st x in [.a,b.] holds
(F | [.a,b.]) . x = integral (f,a,x)
proof
let x be
Real;
( x in [.a,b.] implies (F | [.a,b.]) . x = integral (f,a,x) )
assume A15:
x in [.a,b.]
;
(F | [.a,b.]) . x = integral (f,a,x)
then
(F | [.a,b.]) . x = F . x
by FUNCT_1:49;
hence
(F | [.a,b.]) . x = integral (
f,
a,
x)
by A15, A5;
verum
end;
( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] )
by A2, A3, A6, INTEGRA5:10, INTEGRA5:11;
then
F | ].a,b.] is Lipschitzian
by A8, A1, A2, A13, A14, Th33, FCONT_1:33;
hence
( F is_left_differentiable_in b & Ldiff (F,b) = lim_left ((F `| ].a,b.[),b) )
by A1, A9, A11, A12, Th5; verum