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 )
A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A7: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A8: ( dom (F | ].a,b.[) = ].a,b.[ & dom (f | ].a,b.[) = ].a,b.[ ) by A2, A4, XBOOLE_1:1, RELAT_1:62;
deffunc H₁( Real) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider G1 being Function of REAL,REAL such that
A9: for h being Element of REAL holds G1 . h = H₁(h) from FUNCT_2:sch 4();
reconsider G = G1 | ].a,b.[ as PartFunc of REAL,REAL ;
dom G1 = REAL by FUNCT_2:def 1;
then A10: dom G = ].a,b.[ by RELAT_1:62;

A11: now :: thesis: for x being Real st x in ].a,b.[ holds
G . x = integral (f,a,x)

let x be Real; :: thesis: ( x in ].a,b.[ implies G . x = integral (f,a,x) )
A12: x is Element of REAL by XREAL_0:def 1;
assume x in ].a,b.[ ; :: thesis: G . x = integral (f,a,x)
then G . x = G1 . x by A10, FUNCT_1:47;
then G . x = H₁(x) by A9, A12;
hence G . x = integral (f,a,x) ; :: thesis: verum

end;

A13: now :: thesis: for x being Element of REAL st x in dom (F | ].a,b.[) holds
(F | ].a,b.[) . x = G . x

let x be Element of REAL ; :: thesis: ( x in dom (F | ].a,b.[) implies (F | ].a,b.[) . x = G . x )
assume A14: x in dom (F | ].a,b.[) ; :: thesis: (F | ].a,b.[) . x = G . x
(F | ].a,b.[) . x = F . x by A14, FUNCT_1:47;
then (F | ].a,b.[) . x = integral (f,a,x) by A5, A14, A7, A8;
hence (F | ].a,b.[) . x = G . x by A11, A8, A14; :: thesis: verum

end;

A15: for x being Real st x in ].a,b.[ holds
( G is_differentiable_in x & diff (G,x) = f . x )

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies ( G is_differentiable_in x & diff (G,x) = f . x ) )
A16: f | ].a,b.[ is continuous by A3, FCONT_1:16, XXREAL_1:25;
assume A17: x in ].a,b.[ ; :: thesis: ( G is_differentiable_in x & diff (G,x) = f . x )
then ( a < x & x < b ) by XXREAL_1:4;
then a < b by XXREAL_0:2;
then A18: ( inf ].a,b.[ = a & sup ].a,b.[ = b ) by XXREAL_2:28, XXREAL_2:32;
].a,b.[ c= dom f by A7, A2;
then A19: f is_continuous_in x by A16, A17, A18, Th6;
( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A2, A3, A6, INTEGRA5:10, INTEGRA5:11;
hence ( G is_differentiable_in x & diff (G,x) = f . x ) by A1, A2, A10, A11, A6, A17, A19, INTEGRA6:28; :: thesis: verum

end;

A20: F | ].a,b.[ = G by A8, A10, A13, PARTFUN1:5;
thus for x being Real st x in ].a,b.[ holds
( F is_differentiable_in x & diff (F,x) = f . x ) :: thesis: verum

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies ( F is_differentiable_in x & diff (F,x) = f . x ) )
assume A21: x in ].a,b.[ ; :: thesis: ( F is_differentiable_in x & diff (F,x) = f . x )
then A22: ( G is_differentiable_in x & diff (G,x) = f . x ) by A15;
hence F is_differentiable_in x by A20, A21, PDIFFEQ1:2; :: thesis: diff (F,x) = f . x
hence diff (F,x) = f . x by A20, A21, A22, PDIFFEQ1:2; :: thesis: verum

end;