let a, b be real number ; :: thesis: for f, F being PartFunc of REAL ,REAL
for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds
F . x = (integral f,x0,x) + (F . x0)
let f, F be PartFunc of REAL ,REAL ; :: thesis: for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds
F . x = (integral f,x0,x) + (F . x0)
let x, x0 be real number ; :: thesis: ( f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ implies F . x = (integral f,x0,x) + (F . x0) )
set O = ].a,b.[;
assume that
A1: f | [.a,b.] is continuous and
A2: [.a,b.] c= dom f and
A3: ( x in ].a,b.[ & x0 in ].a,b.[ ) and
A4: F is_integral_of f,].a,b.[ ; :: thesis: F . x = (integral f,x0,x) + (F . x0)
A5: ( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ ) by A4, Lm1;
A6: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A7: [.x,x0.] c= ].a,b.[ by A3, XXREAL_2:def 12;

A8: now

assume A9: x < x0 ; :: thesis: F . x = (integral f,x0,x) + (F . x0)
then A10: ['x,x0'] c= ].a,b.[ by A7, INTEGRA5:def 4;
then A11: f | ['x,x0'] is continuous by A1, A6, FCONT_1:17, XBOOLE_1:1;
(F `| ].a,b.[) || ['x,x0'] = (f | ].a,b.[) | ['x,x0'] by A4, Lm1;
then A12: (F `| ].a,b.[) || ['x,x0'] = f || ['x,x0'] by A10, FUNCT_1:82;
A13: ['x,x0'] c= [.a,b.] by A6, A10, XBOOLE_1:1;
then ['x,x0'] c= dom f by A2, XBOOLE_1:1;
then f is_integrable_on ['x,x0'] by A11, INTEGRA5:17;
then f || ['x,x0'] is integrable by INTEGRA5:def 2;
then A14: F `| ].a,b.[ is_integrable_on ['x,x0'] by A12, INTEGRA5:def 2;
(F `| ].a,b.[) | ['x,x0'] is bounded by A2, A12, A13, A11, INTEGRA5:10, XBOOLE_1:1;
then F . x0 = (integral (f | ].a,b.[),x,x0) + (F . x) by A5, A9, A10, A14, Th10;
then F . x0 = (integral (f | ].a,b.[),['x,x0']) + (F . x) by A9, INTEGRA5:def 5;
then F . x0 = (integral f,['x,x0']) + (F . x) by A10, FUNCT_1:82;
then A15: F . x0 = (integral f,x,x0) + (F . x) by A9, INTEGRA5:def 5;
integral f,x0,x = - (integral f,['x,x0']) by A9, INTEGRA5:def 5;
then integral f,x0,x = - (integral f,x,x0) by A9, INTEGRA5:def 5;
hence F . x = (integral f,x0,x) + (F . x0) by A15; :: thesis: verum

end;

A16: [.x0,x.] c= ].a,b.[ by A3, XXREAL_2:def 12;

now

assume A17: x0 <= x ; :: thesis: F . x = (integral f,x0,x) + (F . x0)
then A18: ['x0,x'] c= ].a,b.[ by A16, INTEGRA5:def 4;
then A19: f | ['x0,x'] is continuous by A1, A6, FCONT_1:17, XBOOLE_1:1;
(F `| ].a,b.[) || ['x0,x'] = (f | ].a,b.[) | ['x0,x'] by A4, Lm1;
then A20: (F `| ].a,b.[) || ['x0,x'] = f || ['x0,x'] by A18, FUNCT_1:82;
['x0,x'] c= [.a,b.] by A6, A18, XBOOLE_1:1;
then A21: ['x0,x'] c= dom f by A2, XBOOLE_1:1;
f | ['x0,x'] is continuous by A1, A6, A18, FCONT_1:17, XBOOLE_1:1;
then f is_integrable_on ['x0,x'] by A21, INTEGRA5:17;
then f || ['x0,x'] is integrable by INTEGRA5:def 2;
then F `| ].a,b.[ is_integrable_on ['x0,x'] by A20, INTEGRA5:def 2;
then F . x = (integral (f | ].a,b.[),x0,x) + (F . x0) by A5, A17, A18, A20, A21, A19, Th10, INTEGRA5:10;
then F . x = (integral (f | ].a,b.[),['x0,x']) + (F . x0) by A17, INTEGRA5:def 5;
then F . x = (integral f,['x0,x']) + (F . x0) by A18, FUNCT_1:82;
hence F . x = (integral f,x0,x) + (F . x0) by A17, INTEGRA5:def 5; :: thesis: verum

end;

hence F . x = (integral f,x0,x) + (F . x0) by A8; :: thesis: verum