let a, b be real number ; :: thesis:
let f, F be PartFunc of REAL ,REAL ; :: thesis:
set O = ].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 number st x in ].a,b.[ holds
F . x = (integral f,a,x) + (F . a) ; :: thesis:
['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
then A6: ].a,b.[ c= ['a,b'] by XXREAL_1:25;
then A7: ].a,b.[ c= dom f by A2, XBOOLE_1:1;
deffunc H₁( Element of REAL ) -> Element of REAL = integral f,a,$1;
consider G1 being Function of REAL ,REAL such that
A8: for h being Real holds G1 . h = H₁(h) from FUNCT_2:sch 4();
reconsider G = G1 | ].a,b.[ as PartFunc of REAL ,REAL ;
dom G = (dom G1) /\ ].a,b.[ by RELAT_1:90;
then A9: dom G = REAL /\ ].a,b.[ by FUNCT_2:def 1;
then A10: ].a,b.[ = dom G by XBOOLE_1:28;

A11: now

let x be real number ; :: thesis:
reconsider z = x as Real by XREAL_0:def 1;
assume x in ].a,b.[ ; :: thesis:
then G . x = G1 . x by A10, FUNCT_1:70;
then G . x = integral f,a,z by A8;
hence G . x = integral f,a,x ; :: thesis:

end;

let x be Real; :: thesis:
assume A13: x in ].a,b.[ ; :: thesis:
then x in dom f by A7;
then B13: x in dom (f | ].a,b.[) by A13, RELAT_1:86;
reconsider z = x as real number ;
f | ].a,b.[ is continuous by A3, A6, FCONT_1:17;
then A14: f | ].a,b.[ is_continuous_in z by B13, FCONT_1:def 2;
A15: ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A3, A2, INTEGRA5:10, INTEGRA5:11;
for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - z) < s holds
abs ((f . x1) - (f . z)) < r ) )

let r be real number ; :: thesis:
assume 0 < r ; :: thesis:
then consider s being real number such that
A16: ( 0 < s & ( for x1 being real number st x1 in dom (f | ].a,b.[) & abs (x1 - z) < s holds
abs (((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)) < r ) ) by A14, FCONT_1:3;
consider ss1 being real number such that
A17: ( 0 < ss1 & ].(z - ss1),(z + ss1).[ c= ].a,b.[ ) by A13, RCOMP_1:40;
set s1 = min ss1,s;
take min ss1,s ; :: thesis:

let x1 be real number ; :: thesis:
assume A18: ( x1 in dom f & abs (x1 - z) < min ss1,s ) ; :: thesis:
min ss1,s <= s by XXREAL_0:17;
then A19: abs (x1 - z) < s by A18, XXREAL_0:2;
min ss1,s <= ss1 by XXREAL_0:17;
then abs (x1 - z) < ss1 by A18, XXREAL_0:2;
then A20: x1 in ].(z - ss1),(z + ss1).[ by RCOMP_1:8;
].a,b.[ = ].a,b.[ /\ (dom f) by A2, A6, XBOOLE_1:1, XBOOLE_1:28;
then A21: ].a,b.[ = dom (f | ].a,b.[) by PARTFUN2:32;
then abs ((f . x1) - (f . z)) = abs (((f | ].a,b.[) . x1) - (f . z)) by A17, A20, FUNCT_1:70;
then abs ((f . x1) - (f . z)) = abs (((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)) by A13, A21, FUNCT_1:70;
hence abs ((f . x1) - (f . z)) < r by A16, A17, A19, A20, A21; :: thesis:

end;

hence ( 0 < min ss1,s & ( for x1 being real number st x1 in dom f & abs (x1 - z) < min ss1,s holds
abs ((f . x1) - (f . z)) < r ) ) by A16, A17, XXREAL_0:15; :: thesis:

end;

then f is_continuous_in z by FCONT_1:3;
hence ( G is_differentiable_in x & diff G,x = f . x ) by A1, A2, A10, A11, A13, A15, INTEGRA6:28; :: thesis:

end;

then for x being Real st x in ].a,b.[ holds
G is_differentiable_in x ;
then A22: G is_differentiable_on ].a,b.[ by A10, FDIFF_1:16;
set H1 = REAL --> (F . a);
A23: for h being Real holds (REAL --> (F . a)) . h = F . a by FUNCOP_1:13;
reconsider H = (REAL --> (F . a)) | ].a,b.[ as PartFunc of REAL ,REAL ;
dom H = (dom (REAL --> (F . a))) /\ ].a,b.[ by RELAT_1:90;
then A24: dom H = REAL /\ ].a,b.[ by FUNCT_2:def 1;
then A25: dom H = ].a,b.[ by XBOOLE_1:28;

let x be Element of REAL ; :: thesis:
assume A26: x in ].a,b.[ /\ (dom H) ; :: thesis:
reconsider z = x as real number ;
H . x = (REAL --> (F . a)) . z by A25, A26, FUNCT_1:70;
then H . x = F . a by A23;
hence H /. x = F . a by A25, A26, PARTFUN1:def 8; :: thesis:

end;

then A27: H | ].a,b.[ is V8() by PARTFUN2:54;
then A28: ( H is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
(H `| ].a,b.[) . x = 0 ) ) by A25, FDIFF_1:30;
dom (F | ].a,b.[) = (dom F) /\ ].a,b.[ by PARTFUN2:32;
then A29: dom (F | ].a,b.[) = ].a,b.[ by A4, XBOOLE_1:28;
then A30: dom (F | ].a,b.[) = (dom G) /\ (dom H) by A9, A24, XBOOLE_1:28;

let x be set ; :: thesis:
assume A31: x in dom (F | ].a,b.[) ; :: thesis:
then reconsider z = x as real number ;
(F | ].a,b.[) . x = F . z by A31, FUNCT_1:70;
then A32: (F | ].a,b.[) . x = (integral f,a,z) + (F . a) by A5, A29, A31;
reconsider z1 = z as Real by XREAL_0:def 1;
H . x = (REAL --> (F . a)) . z1 by A25, A29, A31, FUNCT_1:70;
then H . x = F . a by A23;
hence (F | ].a,b.[) . x = (G . x) + (H . x) by A11, A29, A31, A32; :: thesis:

end;

then A33: F | ].a,b.[ = G + H by A30, VALUED_1:def 1;
then ( F | ].a,b.[ is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
((F | ].a,b.[) `| ].a,b.[) . x = (diff G,x) + (diff H,x) ) ) by A22, A28, A29, FDIFF_1:26;
then for x being Real st x in ].a,b.[ holds
F | ].a,b.[ is_differentiable_in x by FDIFF_1:16;
then A34: F is_differentiable_on ].a,b.[ by A4, FDIFF_1:def 7;
then dom (F `| ].a,b.[) = ].a,b.[ by FDIFF_1:def 8;
then dom (F `| ].a,b.[) = ].a,b.[ /\ (dom f) by A2, A6, XBOOLE_1:1, XBOOLE_1:28;
then A35: dom (F `| ].a,b.[) = dom (f | ].a,b.[) by PARTFUN2:32;

let x be Real; :: thesis:
assume x in dom (F `| ].a,b.[) ; :: thesis:
then A36: x in ].a,b.[ by A34, FDIFF_1:def 8;
then x in (dom f) /\ ].a,b.[ by A7, XBOOLE_0:def 4;
then A37: x in dom (f | ].a,b.[) by PARTFUN2:32;
(F `| ].a,b.[) . x = ((F | ].a,b.[) `| ].a,b.[) . x by A34, FDIFF_2:16;
then (F `| ].a,b.[) . x = (diff G,x) + (diff H,x) by A22, A28, A29, A33, A36, FDIFF_1:26;
then A38: (F `| ].a,b.[) . x = (f . x) + (diff H,x) by A12, A36;
(H `| ].a,b.[) . x = 0 by A25, A27, A36, FDIFF_1:30;
then diff H,x = 0 by A28, A36, FDIFF_1:def 8;
hence (F `| ].a,b.[) . x = (f | ].a,b.[) . x by A37, A38, FUNCT_1:70; :: thesis:

end;

then F `| ].a,b.[ = f | ].a,b.[ by A35, PARTFUN1:34;
hence F is_integral_of f,].a,b.[ by A34, Lm1; :: thesis: