let a, b be real number ; :: thesis: for f being PartFunc of REAL ,REAL
for x0 being real number
for F being PartFunc of REAL ,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff F,x0 = f . x0 )
let f be PartFunc of REAL ,REAL ; :: thesis: for x0 being real number
for F being PartFunc of REAL ,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff F,x0 = f . x0 )
let x0 be real number ; :: thesis: for F being PartFunc of REAL ,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff F,x0 = f . x0 )
let F be PartFunc of REAL ,REAL ; :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & x0 in ].a,b.[ & f is_continuous_in x0 implies ( F is_differentiable_in x0 & diff F,x0 = f . x0 ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) & x0 in ].a,b.[ & f is_continuous_in x0 ) ; :: thesis: ( F is_differentiable_in x0 & diff F,x0 = f . x0 )
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 4;
deffunc H₁( Element of REAL ) -> Element of REAL = (f . x0) * $1;
consider L being Function of REAL ,REAL such that
A3: for h being Real holds L . h = H₁(h) from FUNCT_2:sch 4();
reconsider L = L as PartFunc of REAL ,REAL ;
deffunc H₂( set ) -> Element of REAL = ((F . (x0 + (R_id $1))) - (F . x0)) - (L . (R_id $1));
deffunc H₃( set ) -> Element of NAT = 0 ;
defpred S₁[ set ] means x0 + (R_id $1) in ].a,b.[;
consider R being Function such that
A4: ( dom R = REAL & ( for x being set st x in REAL holds
( ( S₁[x] implies R . x = H₂(x) ) & ( not S₁[x] implies R . x = H₃(x) ) ) ) ) from PARTFUN1:sch 1();
rng R c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng R or y in REAL )
assume y in rng R ; :: thesis: y in REAL
then consider x being set such that
A5: ( x in dom R & y = R . x ) by FUNCT_1:def 5;
( ( S₁[x] implies R . x = H₂(x) ) & ( not S₁[x] implies R . x = H₃(x) ) ) by A4, A5;
hence y in REAL by A5; :: thesis: verum

end;

then reconsider R = R as PartFunc of REAL ,REAL by A4, RELSET_1:11;
reconsider L = L as LINEAR by A3, FDIFF_1:def 4;
A6: R is total by A4, PARTFUN1:def 4;
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 )
A7: for e being real number st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e

proof

let e0 be real number ; :: thesis: ( 0 < e0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0 )
set e = e0 / 2;
assume 0 < e0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0
then A8: ( 0 < e0 / 2 & e0 / 2 < e0 ) by XREAL_1:217, XREAL_1:218;
then consider p being real number such that
A9: ( 0 < p & ( for t being real number st t in dom f & abs (t - x0) < p holds
abs ((f . t) - (f . x0)) < e0 / 2 ) ) by A1, FCONT_1:3;
consider N being Neighbourhood of x0 such that
A10: N c= ].a,b.[ by A1, RCOMP_1:39;
consider q being real number such that
A11: ( 0 < q & N = ].(x0 - q),(x0 + q).[ ) by RCOMP_1:def 7;
set r = min (p / 2),(q / 2);
A12: ( 0 < p / 2 & 0 < q / 2 & p / 2 < p & q / 2 < q ) by A9, A11, XREAL_1:217, XREAL_1:218;
then A13: ( 0 < min (p / 2),(q / 2) & min (p / 2),(q / 2) <= p / 2 & min (p / 2),(q / 2) <= q / 2 ) by XXREAL_0:15, XXREAL_0:17;
then A14: ].(x0 - (min (p / 2),(q / 2))),(x0 + (min (p / 2),(q / 2))).[ c= ].(x0 - q),(x0 + q).[ by A12, Th2, XXREAL_0:2;
A15: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < min (p / 2),(q / 2) by A13, SEQ_2:def 7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0 )
assume n <= m ; :: thesis: abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0
then A17: abs ((h . m) - 0 ) < min (p / 2),(q / 2) by A16;
then abs ((x0 + (h . m)) - x0) < min (p / 2),(q / 2) ;
then x0 + (h . m) in ].(x0 - (min (p / 2),(q / 2))),(x0 + (min (p / 2),(q / 2))).[ by RCOMP_1:8;
then x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A14;
then A18: ( x0 + (h . m) in ].a,b.[ & F . (x0 + (h . m)) = integral f,a,(x0 + (h . m)) ) by A1, A10, A11;
then x0 + (R_id (h . m)) in ].a,b.[ by RSSPACE:def 3;
then R . (h . m) = ((F . (x0 + (R_id (h . m)))) - (F . x0)) - (L . (R_id (h . m))) by A4;
then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (R_id (h . m))) by RSSPACE:def 3;
then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)) by RSSPACE:def 3;
then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A3;
then A19: R . (h . m) = ((integral f,a,(x0 + (h . m))) - (integral f,a,x0)) - ((f . x0) * (h . m)) by A1, A18;
set g = REAL --> (f . x0);
A20: for h being Real holds (REAL --> (f . x0)) . h = f . x0 by FUNCOP_1:13;
A21: dom (REAL --> (f . x0)) = REAL by FUNCT_2:def 1;
A22: for x being real number st x in ['a,b'] holds
(REAL --> (f . x0)) . x = f . x0 by A20;
then A23: ( REAL --> (f . x0) is_integrable_on ['a,b'] & (REAL --> (f . x0)) | ['a,b'] is bounded ) by A1, A21, Th26;
then (f - (REAL --> (f . x0))) | (['a,b'] /\ ['a,b']) is bounded by A1, RFUNCT_1:101;
then A24: ( f - (REAL --> (f . x0)) is_integrable_on ['a,b'] & (f - (REAL --> (f . x0))) | ['a,b'] is bounded ) by A1, A21, A23, Th11;
['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f . x0))) by A1, A21, XBOOLE_1:27;
then A25: ['a,b'] c= dom (f - (REAL --> (f . x0))) by VALUED_1:12;
for x being real number st x in ['(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m)))'] holds
abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2

proof

let x be real number ; :: thesis: ( x in ['(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m)))'] implies abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 )
assume A26: x in ['(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m)))'] ; :: thesis: abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2
reconsider x1 = x as Real by XREAL_0:def 1;
( min x0,(x0 + (h . m)) <= x0 & x0 <= max x0,(x0 + (h . m)) ) by XXREAL_0:17, XXREAL_0:25;
then A27: x in [.(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m))).] by A26, INTEGRA5:def 4, XXREAL_0:2;
abs (x - x0) <= abs (h . m)

proof

per cases ( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) ) ;

suppose x0 <= x0 + (h . m) ; :: thesis: abs (x - x0) <= abs (h . m)

then ( x0 = min x0,(x0 + (h . m)) & x0 + (h . m) = max x0,(x0 + (h . m)) ) by XXREAL_0:def 9, XXREAL_0:def 10;
then x in { z where z is Real : ( x0 <= z & z <= x0 + (h . m) ) } by A27, RCOMP_1:def 1;
then A28: ex z being Real st
( x = z & x0 <= z & z <= x0 + (h . m) ) ;
then A29: x - x0 <= (x0 + (h . m)) - x0 by XREAL_1:11;
then A30: 0 <= h . m by A28, XREAL_1:50;
0 <= x - x0 by A28, XREAL_1:50;
then abs (x - x0) = x - x0 by ABSVALUE:def 1;
hence abs (x - x0) <= abs (h . m) by A29, A30, ABSVALUE:def 1; :: thesis: verum

end;

suppose A31: not x0 <= x0 + (h . m) ; :: thesis: abs (x - x0) <= abs (h . m)

then ( x0 = max x0,(x0 + (h . m)) & x0 + (h . m) = min x0,(x0 + (h . m)) ) by XXREAL_0:def 9, XXREAL_0:def 10;
then x in { z where z is Real : ( x0 + (h . m) <= z & z <= x0 ) } by A27, RCOMP_1:def 1;
then A32: ex z being Real st
( x = z & x0 + (h . m) <= z & z <= x0 ) ;
then A33: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:11;

per cases ( x - x0 <> 0 or x - x0 = 0 ) ;

suppose x - x0 <> 0 ; :: thesis: abs (x - x0) <= abs (h . m)

then x - x0 < 0 by A32, XREAL_1:49;
then A34: abs (x - x0) = - (x - x0) by ABSVALUE:def 1;
(x0 + (h . m)) - x0 < x0 - x0 by A31, XREAL_1:16;
then abs (h . m) = - (h . m) by ABSVALUE:def 1;
hence abs (x - x0) <= abs (h . m) by A33, A34, XREAL_1:26; :: thesis: verum

end;

suppose x - x0 = 0 ; :: thesis: abs (x - x0) <= abs (h . m)

then abs (x - x0) = 0 by ABSVALUE:def 1;
hence abs (x - x0) <= abs (h . m) by COMPLEX1:132; :: thesis: verum

end;

end;

end;

end;

end;

then A35: abs (x - x0) < min (p / 2),(q / 2) by A17, XXREAL_0:2;
then abs (x - x0) < p / 2 by A13, XXREAL_0:2;
then A36: abs (x - x0) < p by A12, XXREAL_0:2;
x in ].(x0 - (min (p / 2),(q / 2))),(x0 + (min (p / 2),(q / 2))).[ by A35, RCOMP_1:8;
then x in ].(x0 - q),(x0 + q).[ by A14;
then x in ].a,b.[ by A10, A11;
then A37: x in [.a,b.] by A15;
then abs ((f . x) - (f . x0)) <= e0 / 2 by A1, A2, A9, A36;
then abs ((f . x1) - ((REAL --> (f . x0)) . x1)) <= e0 / 2 by A20;
hence abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 by A2, A25, A37, VALUED_1:13; :: thesis: verum

end;

then A38: abs (integral (f - (REAL --> (f . x0))),x0,(x0 + (h . m))) <= (e0 / 2) * (abs ((x0 + (h . m)) - x0)) by A1, A2, A15, A18, A24, A25, Lm8;
h is non-zero by FDIFF_1:def 1;
then h . m <> 0 by SEQ_1:6;
then A39: 0 < abs (h . m) by COMPLEX1:133;
A40: abs ((R . (h . m)) / (h . m)) = (abs (R . (h . m))) / (abs (h . m)) by COMPLEX1:153;
A41: integral (REAL --> (f . x0)),x0,(x0 + (h . m)) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A2, A15, A18, A21, A22, Th27;
integral f,a,(x0 + (h . m)) = (integral f,a,x0) + (integral f,x0,(x0 + (h . m))) by A1, A2, A15, A18, Th20;
then R . (h . m) = integral (f - (REAL --> (f . x0))),x0,(x0 + (h . m)) by A1, A2, A15, A18, A19, A21, A23, A41, Th24;
then (abs (R . (h . m))) / (abs (h . m)) <= ((e0 / 2) * (abs (h . m))) / (abs (h . m)) by A38, A39, XREAL_1:74;
then A42: abs ((R . (h . m)) / (h . m)) <= e0 / 2 by A39, A40, XCMPLX_1:90;
rng h c= dom R by A4;
then (R . (h . m)) / (h . m) = ((R /* h) . m) / (h . m) by FUNCT_2:185;
then (R . (h . m)) / (h . m) = ((R /* h) . m) * ((h " ) . m) by VALUED_1:10;
then (R . (h . m)) / (h . m) = ((h " ) (#) (R /* h)) . m by SEQ_1:12;
hence abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0 by A8, A42, XXREAL_0:2; :: thesis: verum

end;

hence (h " ) (#) (R /* h) is convergent by SEQ_2:def 6; :: thesis: lim ((h " ) (#) (R /* h)) = 0
hence lim ((h " ) (#) (R /* h)) = 0 by A7, SEQ_2:def 7; :: thesis: verum

end;

then reconsider R = R as REST by A6, FDIFF_1:def 3;
consider N being Neighbourhood of x0 such that
A43: N c= ].a,b.[ by A1, RCOMP_1:39;
A44: N c= dom F by A1, A43, XBOOLE_1:1;
A45: for x being Real st x in N holds
(F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A46: x in N ; :: thesis: (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))
A47: x0 + (R_id (x - x0)) = x0 + (x - x0) by RSSPACE:def 3;
x0 + (x - x0) in N by A46;
then x0 + (R_id (x - x0)) in N by RSSPACE:def 3;
then R . (x - x0) = H₂(x - x0) by A4, A43;
hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) by A47; :: thesis: verum

end;

hence A48: F is_differentiable_in x0 by A44, FDIFF_1:def 5; :: thesis: diff F,x0 = f . x0
L . 1 = (f . x0) * 1 by A3;
hence diff F,x0 = f . x0 by A44, A45, A48, FDIFF_1:def 6; :: thesis: verum