let a, b be Real; :: thesis: 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
for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x )
let f, F be PartFunc of REAL,REAL; :: thesis: ( 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 for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x ) )
set O = ].a,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) ; :: thesis: for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x )
reconsider I = ['a,b'] as non empty Interval ;
A6: I = [.a,b.] by A1, INTEGRA5:def 3;
then A7: ( inf I = a & sup I = b ) by A1, XXREAL_2:25, XXREAL_2:29;
A8: ( F is_differentiable_on_interval ['a,b'] & F `\ ['a,b'] = f | ['a,b'] ) by A1, A2, A3, A4, A5, Th37;
then A9: F is_differentiable_on ].a,b.[ by A7, FDIFF_12:def 1;

hereby :: thesis: verum

let x be Real; :: thesis: ( x in ].a,b.[ implies ( F is_differentiable_in x & diff (F,x) = f . x ) )
assume A10: x in ].a,b.[ ; :: thesis: ( F is_differentiable_in x & diff (F,x) = f . x )
hence F is_differentiable_in x by A9, FDIFF_1:9; :: thesis: diff (F,x) = f . x
A11: ].a,b.[ c= ['a,b'] by A6, XXREAL_1:25;
( inf I < x & x < sup I ) by A7, A10, XXREAL_1:4;
then (F `\ ['a,b']) . x = diff (F,x) by A8, A10, A11, FDIFF_12:def 2;
hence diff (F,x) = f . x by A8, A10, A11, FUNCT_1:49; :: thesis: verum

end;