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
A0: [.a,b.] c= dom f and
A2: ( x in ].a,b.[ & x0 in ].a,b.[ ) and
A3: F is_integral_of f,].a,b.[ ; :: thesis: F . x = (integral f,x0,x) + (F . x0)
A4: ( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ ) by A3, Lm1;
A5: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A6: ( [.x0,x.] c= ].a,b.[ & [.x,x0.] c= ].a,b.[ ) by A2, XXREAL_2:def 12;

A7: now

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

end;

now

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

end;

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