let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )
let f be PartFunc of REAL,REAL; :: thesis: ( a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous implies ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ ) )
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f | [.a,b.] is continuous ; :: thesis: ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )
consider x0 being Real such that
A4: ( a < x0 & x0 < b ) by A1, XREAL_1:5;
A5: x0 in ].a,b.[ by A4, XXREAL_1:4;
A6: [.a,b.] = ['a,b'] by A1, INTEGRA5:def 3;
then A7: f | ['a,b'] is bounded by A2, A3, INTEGRA5:10;
( a in ['a,b'] & b in ['a,b'] ) by A1, A6, XXREAL_1:1;
then A8: ( inf ['a,b'] <= a & b <= sup ['a,b'] ) by XXREAL_2:3, XXREAL_2:4;
A9: f is_integrable_on ['a,b'] by A2, A3, A6, INTEGRA5:11;
then consider F being PartFunc of REAL,REAL such that
A10: ( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) by A1, A7, A2, A6, A5, A3, A8, Th6, INTEGRA6:29;
for x being Real st x in ].a,b.[ holds
F | ].a,b.[ is_differentiable_in x

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies F | ].a,b.[ is_differentiable_in x )
assume A11: x in ].a,b.[ ; :: thesis: F | ].a,b.[ is_differentiable_in x
then f is_continuous_in x by A2, A3, A6, A8, Th6;
then F is_differentiable_in x by A1, A9, A7, A2, A6, A10, A11, INTEGRA6:28;
hence F | ].a,b.[ is_differentiable_in x by A11, PDIFFEQ1:2; :: thesis: verum

end;

then A12: F is_differentiable_on ].a,b.[ by A10;
then A13: dom (F `| ].a,b.[) = ].a,b.[ by FDIFF_1:def 7;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
then ].a,b.[ c= dom f by A2;
then A14: dom (f | ].a,b.[) = ].a,b.[ by RELAT_1:62;
for x being Element of REAL st x in dom (F `| ].a,b.[) holds
(F `| ].a,b.[) . x = (f | ].a,b.[) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (F `| ].a,b.[) implies (F `| ].a,b.[) . x = (f | ].a,b.[) . x )
assume A15: x in dom (F `| ].a,b.[) ; :: thesis: (F `| ].a,b.[) . x = (f | ].a,b.[) . x
then A16: f is_continuous_in x by A2, A3, A13, A6, A8, Th6;
(F `| ].a,b.[) . x = diff (F,x) by A12, A13, A15, FDIFF_1:def 7;
then (F `| ].a,b.[) . x = f . x by A1, A9, A7, A2, A6, A10, A15, A13, A16, INTEGRA6:28;
hence (F `| ].a,b.[) . x = (f | ].a,b.[) . x by A15, A13, A14, FUNCT_1:47; :: thesis: verum

end;

hence ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ ) by A10, A12, A13, A14, PARTFUN1:5; :: thesis: verum