let a, b be Real; :: thesis: for f, F being PartFunc of REAL,REAL
for x, x0 being Real 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 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; :: 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 :: thesis: ( x < x0 implies F . x = (integral (f,x0,x)) + (F . x0) )

assume A9: x < x0 ; :: thesis: F . x = (integral (f,x0,x)) + (F . x0)
then A10: ['x,x0'] c= ].a,b.[ by A7, INTEGRA5:def 3;
then A11: f | ['x,x0'] is continuous by A1, A6, FCONT_1:16, 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:51;
A13: ['x,x0'] c= [.a,b.] by A6, A10;
then ['x,x0'] c= dom f by A2;
then f is_integrable_on ['x,x0'] by A11, INTEGRA5:17;
then f || ['x,x0'] is integrable ;
then A14: F `| ].a,b.[ is_integrable_on ['x,x0'] by A12;
(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 4;
then F . x0 = (integral (f,['x,x0'])) + (F . x) by A10, FUNCT_1:51;
then A15: F . x0 = (integral (f,x,x0)) + (F . x) by A9, INTEGRA5:def 4;
integral (f,x0,x) = - (integral (f,['x,x0'])) by A9, INTEGRA5:def 4;
then integral (f,x0,x) = - (integral (f,x,x0)) by A9, INTEGRA5:def 4;
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 :: thesis: ( x0 <= x implies F . x = (integral (f,x0,x)) + (F . x0) )

assume A17: x0 <= x ; :: thesis: F . x = (integral (f,x0,x)) + (F . x0)
then A18: ['x0,x'] c= ].a,b.[ by A16, INTEGRA5:def 3;
then A19: f | ['x0,x'] is continuous by A1, A6, FCONT_1:16, 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:51;
['x0,x'] c= [.a,b.] by A6, A18;
then A21: ['x0,x'] c= dom f by A2;
f | ['x0,x'] is continuous by A1, A6, A18, FCONT_1:16, XBOOLE_1:1;
then f is_integrable_on ['x0,x'] by A21, INTEGRA5:17;
then f || ['x0,x'] is integrable ;
then F `| ].a,b.[ is_integrable_on ['x0,x'] by A20;
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 4;
then F . x = (integral (f,['x0,x'])) + (F . x0) by A18, FUNCT_1:51;
hence F . x = (integral (f,x0,x)) + (F . x0) by A17, INTEGRA5:def 4; :: thesis: verum

end;

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