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)) + (F . a) ) holds
F is_integral_of f,].a,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)) + (F . a) ) implies F is_integral_of f,].a,b.[ )
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 st x in ].a,b.[ holds
F . x = (integral (f,a,x)) + (F . a) ; :: thesis: F is_integral_of f,].a,b.[
dom (F | ].a,b.[) = (dom F) /\ ].a,b.[ by PARTFUN2:15;
then A6: dom (F | ].a,b.[) = ].a,b.[ by A4, XBOOLE_1:28;
reconsider Fa = F . a as Element of REAL by XREAL_0:def 1;
set H1 = REAL --> Fa;
deffunc H₁( Real) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider G1 being Function of REAL,REAL such that
A7: for h being Element of REAL holds G1 . h = H₁(h) from FUNCT_2:sch 4();
reconsider H = (REAL --> Fa) | ].a,b.[ as PartFunc of REAL,REAL ;
reconsider G = G1 | ].a,b.[ as PartFunc of REAL,REAL ;
dom H = (dom (REAL --> Fa)) /\ ].a,b.[ by RELAT_1:61;
then A8: dom H = REAL /\ ].a,b.[ by FUNCT_2:def 1;
then A9: dom H = ].a,b.[ by XBOOLE_1:28;

now :: thesis: for x being Element of REAL st x in ].a,b.[ /\ (dom H) holds
H /. x = F . a

let x be Element of REAL ; :: thesis: ( x in ].a,b.[ /\ (dom H) implies H /. x = F . a )
reconsider z = x as Real ;
assume A10: x in ].a,b.[ /\ (dom H) ; :: thesis: H /. x = F . a
then H . x = (REAL --> Fa) . z by A9, FUNCT_1:47;
then H . x = F . a by FUNCOP_1:7;
hence H /. x = F . a by A9, A10, PARTFUN1:def 6; :: thesis: verum

end;

then A11: H | ].a,b.[ is constant by PARTFUN2:35;
then A12: H is_differentiable_on ].a,b.[ by A9, FDIFF_1:22;
dom G = (dom G1) /\ ].a,b.[ by RELAT_1:61;
then A13: dom G = REAL /\ ].a,b.[ by FUNCT_2:def 1;
then A14: ].a,b.[ = dom G by XBOOLE_1:28;

A15: now :: thesis: for x being Real st x in ].a,b.[ holds
G . x = integral (f,a,x)

let x be Real; :: thesis: ( x in ].a,b.[ implies G . x = integral (f,a,x) )
reconsider z = x as Element of REAL by XREAL_0:def 1;
assume x in ].a,b.[ ; :: thesis: G . x = integral (f,a,x)
then G . x = G1 . x by A14, FUNCT_1:47;
then G . x = H₁(z) by A7;
hence G . x = integral (f,a,x) ; :: thesis: verum

end;

A16: now :: thesis: for x being object st x in dom (F | ].a,b.[) holds
(F | ].a,b.[) . x = (G . x) + (H . x)

let x be object ; :: thesis: ( x in dom (F | ].a,b.[) implies (F | ].a,b.[) . x = (G . x) + (H . x) )
assume A17: x in dom (F | ].a,b.[) ; :: thesis: (F | ].a,b.[) . x = (G . x) + (H . x)
then reconsider z = x as Real ;
reconsider z1 = z as Element of REAL by XREAL_0:def 1;
H . x = (REAL --> Fa) . z1 by A9, A6, A17, FUNCT_1:47;
then A18: H . x = F . a by FUNCOP_1:7;
(F | ].a,b.[) . x = F . z by A17, FUNCT_1:47;
then (F | ].a,b.[) . x = (integral (f,a,z)) + (F . a) by A5, A6, A17;
hence (F | ].a,b.[) . x = (G . x) + (H . x) by A15, A6, A17, A18; :: thesis: verum

end;

A19: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A20: ].a,b.[ c= ['a,b'] by XXREAL_1:25;
then A21: ].a,b.[ c= dom f by A2;
A22: for x being Real st x in ].a,b.[ holds
( G is_differentiable_in x & diff (G,x) = f . x )

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies ( G is_differentiable_in x & diff (G,x) = f . x ) )
reconsider z = x as Real ;
A23: f | ].a,b.[ is continuous by A3, A19, FCONT_1:16, XXREAL_1:25;
assume A24: x in ].a,b.[ ; :: thesis: ( G is_differentiable_in x & diff (G,x) = f . x )
then x in dom (f | ].a,b.[) by A21, RELAT_1:57;
then A25: f | ].a,b.[ is_continuous_in z by A23;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - z).| < s holds
|.((f . x1) - (f . z)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - z).| < s holds
|.((f . x1) - (f . z)).| < r ) ) )
consider ss1 being Real such that
A26: 0 < ss1 and
A27: ].(z - ss1),(z + ss1).[ c= ].a,b.[ by A24, RCOMP_1:19;
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - z).| < s holds
|.((f . x1) - (f . z)).| < r ) )
then consider s being Real such that
A28: 0 < s and
A29: for x1 being Real st x1 in dom (f | ].a,b.[) & |.(x1 - z).| < s holds
|.(((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)).| < r by A25, FCONT_1:3;
set s1 = min (ss1,s);
take min (ss1,s) ; :: thesis: ( 0 < min (ss1,s) & ( for x1 being Real st x1 in dom f & |.(x1 - z).| < min (ss1,s) holds
|.((f . x1) - (f . z)).| < r ) )

now :: thesis: for x1 being Real st x1 in dom f & |.(x1 - z).| < min (ss1,s) holds
|.((f . x1) - (f . z)).| < r

let x1 be Real; :: thesis: ( x1 in dom f & |.(x1 - z).| < min (ss1,s) implies |.((f . x1) - (f . z)).| < r )
assume that
x1 in dom f and
A30: |.(x1 - z).| < min (ss1,s) ; :: thesis: |.((f . x1) - (f . z)).| < r
min (ss1,s) <= s by XXREAL_0:17;
then A31: |.(x1 - z).| < s by A30, XXREAL_0:2;
].a,b.[ = ].a,b.[ /\ (dom f) by A2, A20, XBOOLE_1:1, XBOOLE_1:28;
then A32: ].a,b.[ = dom (f | ].a,b.[) by PARTFUN2:15;
min (ss1,s) <= ss1 by XXREAL_0:17;
then |.(x1 - z).| < ss1 by A30, XXREAL_0:2;
then A33: x1 in ].(z - ss1),(z + ss1).[ by RCOMP_1:1;
then |.((f . x1) - (f . z)).| = |.(((f | ].a,b.[) . x1) - (f . z)).| by A27, A32, FUNCT_1:47;
then |.((f . x1) - (f . z)).| = |.(((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)).| by A24, A32, FUNCT_1:47;
hence |.((f . x1) - (f . z)).| < r by A29, A27, A31, A33, A32; :: thesis: verum

end;

hence ( 0 < min (ss1,s) & ( for x1 being Real st x1 in dom f & |.(x1 - z).| < min (ss1,s) holds
|.((f . x1) - (f . z)).| < r ) ) by A28, A26, XXREAL_0:15; :: thesis: verum

end;

then A34: f is_continuous_in z by FCONT_1:3;
( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A2, A3, INTEGRA5:10, INTEGRA5:11;
hence ( G is_differentiable_in x & diff (G,x) = f . x ) by A1, A2, A14, A15, A24, A34, INTEGRA6:28; :: thesis: verum

end;

then for x being Real st x in ].a,b.[ holds
G is_differentiable_in x ;
then A35: G is_differentiable_on ].a,b.[ by A14;
dom (F | ].a,b.[) = (dom G) /\ (dom H) by A13, A8, A6, XBOOLE_1:28;
then A36: F | ].a,b.[ = G + H by A16, VALUED_1:def 1;
then F | ].a,b.[ is_differentiable_on ].a,b.[ by A35, A12, A6, FDIFF_1:18;
then for x being Real st x in ].a,b.[ holds
F | ].a,b.[ is_differentiable_in x ;
then A37: F is_differentiable_on ].a,b.[ by A4;

A38: now :: thesis: for x being Element of REAL st x in dom (F `| ].a,b.[) holds
(F `| ].a,b.[) . x = (f | ].a,b.[) . x

let x be Element of REAL ; :: thesis: ( x in dom (F `| ].a,b.[) implies (F `| ].a,b.[) . x = (f | ].a,b.[) . x )
assume x in dom (F `| ].a,b.[) ; :: thesis: (F `| ].a,b.[) . x = (f | ].a,b.[) . x
then A39: x in ].a,b.[ by A37, FDIFF_1:def 7;
then x in (dom f) /\ ].a,b.[ by A21, XBOOLE_0:def 4;
then A40: x in dom (f | ].a,b.[) by PARTFUN2:15;
(F `| ].a,b.[) . x = ((F | ].a,b.[) `| ].a,b.[) . x by A37, FDIFF_2:16;
then (F `| ].a,b.[) . x = (diff (G,x)) + (diff (H,x)) by A35, A12, A6, A36, A39, FDIFF_1:18;
then A41: (F `| ].a,b.[) . x = (f . x) + (diff (H,x)) by A22, A39;
(H `| ].a,b.[) . x = 0 by A9, A11, A39, FDIFF_1:22;
then diff (H,x) = 0 by A12, A39, FDIFF_1:def 7;
hence (F `| ].a,b.[) . x = (f | ].a,b.[) . x by A40, A41, FUNCT_1:47; :: thesis: verum

end;

dom (F `| ].a,b.[) = ].a,b.[ by A37, FDIFF_1:def 7;
then dom (F `| ].a,b.[) = ].a,b.[ /\ (dom f) by A2, A20, XBOOLE_1:1, XBOOLE_1:28;
then dom (F `| ].a,b.[) = dom (f | ].a,b.[) by PARTFUN2:15;
then F `| ].a,b.[ = f | ].a,b.[ by A38, PARTFUN1:5;
hence F is_integral_of f,].a,b.[ by A37, Lm1; :: thesis: verum