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 `| ].a,b.[ is_right_convergent_in a & F `| ].a,b.[ is_left_convergent_in 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 `| ].a,b.[ is_right_convergent_in a & F `| ].a,b.[ is_left_convergent_in 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 `| ].a,b.[ is_right_convergent_in a & F `| ].a,b.[ is_left_convergent_in b )
A6: [.a,b.] = ['a,b'] by A1, INTEGRA5:def 3;
A7: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A8: ( ].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 A9: 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 A9, PDIFFEQ1:2; :: thesis: verum

end;

then A10: F is_differentiable_on ].a,b.[ by A8;
then A11: dom (F `| ].a,b.[) = ].a,b.[ by FDIFF_1:def 7;
A12: dom (f | ].a,b.[) = ].a,b.[ by A8, 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 A13: x in dom (F `| ].a,b.[) ; :: thesis: (F `| ].a,b.[) . x = (f | ].a,b.[) . x
then (F `| ].a,b.[) . x = diff (F,x) by A11, A10, FDIFF_1:def 7;
then (F `| ].a,b.[) . x = f . x by A11, A13, A1, A2, A3, A4, A5, Th32;
hence (F `| ].a,b.[) . x = (f | ].a,b.[) . x by A11, A13, FUNCT_1:49; :: thesis: verum

end;

then A14: F `| ].a,b.[ = f | ].a,b.[ by A11, A12, PARTFUN1:5;
A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A16: ( a in ['a,b'] & b in ['a,b'] ) by A1, XXREAL_1:1;
A17: for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom (F `| ].a,b.[) )

proof

let r be Real; :: thesis: ( a < r implies ex g being Real st
( g < r & a < g & g in dom (F `| ].a,b.[) ) )
assume a < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom (F `| ].a,b.[) )
then consider g being Real such that
A18: ( a < g & g < min (r,b) ) by A1, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis: ( g < r & a < g & g in dom (F `| ].a,b.[) )
( min (r,b) <= r & min (r,b) <= b ) by XXREAL_0:17;
then ( g < r & g < b ) by A18, XXREAL_0:2;
hence ( g < r & a < g & g in dom (F `| ].a,b.[) ) by A18, A11, XXREAL_1:4; :: thesis: verum

end;

for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 ) ) )
assume 0 < g1 ; :: thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 ) )
then consider s being Real such that
A19: 0 < s and
A20: for x1 being Real st x1 in ['a,b'] & |.(x1 - a).| < s holds
|.((f . x1) - (f . a)).| < g1 by A16, A2, A3, A15, FCONT_1:14;
take r = a + s; :: thesis: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 ) )
thus a < r by A19, XREAL_1:29; :: thesis: for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1
thus for r1 being Real st r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( r1 < r & a < r1 & r1 in dom (F `| ].a,b.[) implies |.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 )
assume that
A21: r1 < r and
A22: a < r1 and
A23: r1 in dom (F `| ].a,b.[) ; :: thesis: |.(((F `| ].a,b.[) . r1) - (f . a)).| < g1
0 < r1 - a by A22, XREAL_1:50;
then A24: |.(r1 - a).| = r1 - a by COMPLEX1:43;
r1 - a < r - a by A21, XREAL_1:14;
then |.((f . r1) - (f . a)).| < g1 by A6, A7, A11, A23, A20, A24;
hence |.(((F `| ].a,b.[) . r1) - (f . a)).| < g1 by A14, A11, A23, FUNCT_1:49; :: thesis: verum

end;

end;

hence F `| ].a,b.[ is_right_convergent_in a by A17, LIMFUNC2:10; :: thesis: F `| ].a,b.[ is_left_convergent_in b
A25: for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (F `| ].a,b.[) )

proof

let r be Real; :: thesis: ( r < b implies ex g being Real st
( r < g & g < b & g in dom (F `| ].a,b.[) ) )
assume r < b ; :: thesis: ex g being Real st
( r < g & g < b & g in dom (F `| ].a,b.[) )
then consider g being Real such that
A26: ( max (a,r) < g & g < b ) by A1, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis: ( r < g & g < b & g in dom (F `| ].a,b.[) )
( a <= max (a,r) & r <= max (a,r) ) by XXREAL_0:25;
then ( r < g & a < g ) by A26, XXREAL_0:2;
hence ( r < g & g < b & g in dom (F `| ].a,b.[) ) by A26, A11, XXREAL_1:4; :: thesis: verum

end;

for g1 being Real st 0 < g1 holds
ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 ) ) )
assume 0 < g1 ; :: thesis: ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 ) )
then consider s being Real such that
A27: 0 < s and
A28: for x1 being Real st x1 in ['a,b'] & |.(x1 - b).| < s holds
|.((f . x1) - (f . b)).| < g1 by A16, A2, A3, A15, FCONT_1:14;
take r = b - s; :: thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 ) )
thus r < b by A27, XREAL_1:44; :: thesis: for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1
thus for r1 being Real st r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) holds
|.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( r < r1 & r1 < b & r1 in dom (F `| ].a,b.[) implies |.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 )
assume that
A29: r < r1 and
A30: r1 < b and
A31: r1 in dom (F `| ].a,b.[) ; :: thesis: |.(((F `| ].a,b.[) . r1) - (f . b)).| < g1
r1 - b < 0 by A30, XREAL_1:49;
then A32: |.(r1 - b).| = - (r1 - b) by COMPLEX1:70;
b - r1 < b - r by A29, XREAL_1:15;
then |.((f . r1) - (f . b)).| < g1 by A11, A31, A6, A7, A28, A32;
hence |.(((F `| ].a,b.[) . r1) - (f . b)).| < g1 by A14, A11, A31, FUNCT_1:49; :: thesis: verum

end;

end;

hence F `| ].a,b.[ is_left_convergent_in b by A25, LIMFUNC2:7; :: thesis: verum