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_interval ['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_interval ['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_interval ['a,b'] & F `\ ['a,b'] = f | ['a,b'] )
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: ( inf I in I implies F is_right_differentiable_in lower_bound I )

proof

assume inf I in I ; :: thesis: F is_right_differentiable_in lower_bound I
then a = lower_bound I by A7, Th1;
hence F is_right_differentiable_in lower_bound I by A1, A2, A3, A4, A5, Th35; :: thesis: verum

end;

A9: ( sup I in I implies F is_left_differentiable_in upper_bound I )

proof

assume sup I in I ; :: thesis: F is_left_differentiable_in upper_bound I
then b = upper_bound I by A7, Th2;
hence F is_left_differentiable_in upper_bound I by A1, A2, A3, A4, A5, Th36; :: thesis: verum

end;

A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A11: ( ].a,b.[ c= dom f & ].a,b.[ c= dom F ) by A2, A4;
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 A12: x in ].a,b.[ ; :: thesis: 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 A12, PDIFFEQ1:2; :: thesis: verum

end;

then A13: F is_differentiable_on ].(inf I),(sup I).[ by A7, A11;
thus A14: F is_differentiable_on_interval ['a,b'] by A1, A4, A6, A7, A8, A9, A13, FDIFF_12:def 1; :: thesis: F `\ ['a,b'] = f | ['a,b']
for x being Real st x in ].a,b.[ holds
F . x = integral (f,a,x) by A5, A10;
then A15: F `| ].a,b.[ = f | ].a,b.[ by A1, A2, A3, A11, Th27;
A16: ( dom (F `\ ['a,b']) = ['a,b'] & dom (f | ['a,b']) = ['a,b'] ) by A2, A6, A14, FDIFF_12:def 2, 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 A17: x in dom (F `\ ['a,b']) ; :: thesis: (F `\ ['a,b']) . x = (f | ['a,b']) . x

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A18: x = inf I ; :: thesis: (F `\ ['a,b']) . x = (f | ['a,b']) . x

then (F `\ ['a,b']) . x = Rdiff (F,x) by A14, A17, A16, FDIFF_12:def 2;
then A19: (F `\ ['a,b']) . x = lim_right ((f | ].a,b.[),a) by A15, A1, A2, A3, A4, A5, A7, A18, Th35;
x in [.a,b.[ by A1, A7, A18, XXREAL_1:3;
then (F `\ ['a,b']) . x = f . x by A19, A2, A3, A7, A18, Th10;
hence (F `\ ['a,b']) . x = (f | ['a,b']) . x by A17, A16, FUNCT_1:49; :: thesis: verum

end;

suppose A20: x = sup I ; :: thesis: (F `\ ['a,b']) . x = (f | ['a,b']) . x

then (F `\ ['a,b']) . x = Ldiff (F,x) by A14, A17, A16, FDIFF_12:def 2;
then A21: (F `\ ['a,b']) . x = lim_left ((f | ].a,b.[),b) by A15, A1, A2, A3, A4, A5, A7, A20, Th36;
x in ].a,b.] by A1, A7, A20, XXREAL_1:2;
then (F `\ ['a,b']) . x = f . x by A21, A2, A3, A7, A20, Th11;
hence (F `\ ['a,b']) . x = (f | ['a,b']) . x by A17, A16, FUNCT_1:49; :: thesis: verum

end;

suppose A22: ( x <> inf I & x <> sup I ) ; :: thesis: (F `\ ['a,b']) . x = (f | ['a,b']) . x

then A23: (F `\ ['a,b']) . x = diff (F,x) by A14, A17, A16, FDIFF_12:def 2;
( a <= x & x <= b ) by A17, A16, A6, XXREAL_1:1;
then ( a < x & x < b ) by A22, A7, XXREAL_0:1;
then x in ].a,b.[ by XXREAL_1:4;
then (F `\ ['a,b']) . x = f . x by A1, A2, A3, A4, A5, A23, Th32;
hence (F `\ ['a,b']) . x = (f | ['a,b']) . x by A17, A16, FUNCT_1:49; :: thesis: verum

end;

end;

end;

hence F `\ ['a,b'] = f | ['a,b'] by A16, PARTFUN1:5; :: thesis: verum