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
( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )
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 ( 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 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: ( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ )
consider G being PartFunc of REAL,REAL such that
A6: ( ].a,b.[ c= dom G & ( for x being Real st x in ].a,b.[ holds
G . x = integral (f,a,x) ) & G is_differentiable_on ].a,b.[ & G `| ].a,b.[ = f | ].a,b.[ ) by A1, A2, A3, Th26;
A7: ( dom (F | ].a,b.[) = ].a,b.[ & dom (G | ].a,b.[) = ].a,b.[ ) by A4, A6, RELAT_1:62;
for x being Element of REAL st x in dom (F | ].a,b.[) holds
(F | ].a,b.[) . x = (G | ].a,b.[) . x

proof

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

end;

then A9: F | ].a,b.[ = G | ].a,b.[ by A7, PARTFUN1:5;
hence F is_differentiable_on ].a,b.[ by A4, A6; :: thesis: F `| ].a,b.[ = f | ].a,b.[
then F `| ].a,b.[ = (F | ].a,b.[) `| ].a,b.[ by PDIFFEQ1:4;
hence F `| ].a,b.[ = f | ].a,b.[ by A6, A9, PDIFFEQ1:4; :: thesis: verum