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 )
deffunc H₁( set ) -> Element of NAT = 0 ;
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 that
A1: a <= b and
A2: f is_integrable_on ['a,b'] and
A3: f | ['a,b'] is bounded and
A4: ['a,b'] c= dom f and
A5: ].a,b.[ c= dom F and
A6: for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x and
A7: x0 in ].a,b.[ and
A8: f is_continuous_in x0 ; :: thesis: ( F is_differentiable_in x0 & diff F,x0 = f . x0 )
defpred S₁[ set ] means x0 + (R_id $1) in ].a,b.[;
deffunc H₂( Element of REAL ) -> Element of REAL = (f . x0) * $1;
consider L being Function of REAL ,REAL such that
A9: 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));
reconsider L = L as LINEAR by A9, FDIFF_1:def 4;
consider R being Function such that
A10: ( 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
A11: x in dom R and
A12: y = R . x by FUNCT_1:def 5;
A13: ( not S₁[x] implies R . x = H₁(x) ) by A10, A11;
( S₁[x] implies R . x = H₃(x) ) by A10, A11;
hence y in REAL by A12, A13; :: thesis: verum

end;

then reconsider R = R as PartFunc of REAL ,REAL by A10, RELSET_1:11;
A14: R is total by A10, PARTFUN1:def 4;
A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
A16: 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 )
A17: 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

set g = REAL --> (f . x0);
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;
A18: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
assume A19: 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 0 < e0 / 2 by XREAL_1:217;
then consider p being real number such that
A20: 0 < p and
A21: for t being real number st t in dom f & abs (t - x0) < p holds
abs ((f . t) - (f . x0)) < e0 / 2 by A8, FCONT_1:3;
A22: 0 < p / 2 by A20, XREAL_1:217;
A23: p / 2 < p by A20, XREAL_1:218;
consider N being Neighbourhood of x0 such that
A24: N c= ].a,b.[ by A7, RCOMP_1:39;
consider q being real number such that
A25: 0 < q and
A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def 7;
A27: q / 2 < q by A25, XREAL_1:218;
set r = min (p / 2),(q / 2);
0 < q / 2 by A25, XREAL_1:217;
then 0 < min (p / 2),(q / 2) by A22, XXREAL_0:15;
then consider n being Element of NAT such that
A28: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < min (p / 2),(q / 2) by A18, 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 )
min (p / 2),(q / 2) <= q / 2 by XXREAL_0:17;
then A29: ].(x0 - (min (p / 2),(q / 2))),(x0 + (min (p / 2),(q / 2))).[ c= ].(x0 - q),(x0 + q).[ by A27, Th2, XXREAL_0:2;
assume n <= m ; :: thesis: abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0
then A30: abs ((h . m) - 0 ) < min (p / 2),(q / 2) by A28;
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 A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29;
then A32: x0 + (h . m) in ].a,b.[ by A24, A26;
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 A10;
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 A33: R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A9;
F . (x0 + (h . m)) = integral f,a,(x0 + (h . m)) by A6, A24, A26, A31;
then A34: R . (h . m) = ((integral f,a,(x0 + (h . m))) - (integral f,a,x0)) - ((f . x0) * (h . m)) by A6, A7, A33;
A35: dom (REAL --> (f . x0)) = REAL by FUNCT_2:def 1;
then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f . x0))) by A4, XBOOLE_1:27;
then A36: ['a,b'] c= dom (f - (REAL --> (f . x0))) by VALUED_1:12;
A37: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A38: integral f,a,(x0 + (h . m)) = (integral f,a,x0) + (integral f,x0,(x0 + (h . m))) by A1, A2, A3, A4, A7, A15, A32, Th20;
A39: min (p / 2),(q / 2) <= p / 2 by XXREAL_0:17;
A40: 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 )
reconsider x1 = x as Real by XREAL_0:def 1;
A41: ( min x0,(x0 + (h . m)) <= x0 & x0 <= max x0,(x0 + (h . m)) ) by XXREAL_0:17, XXREAL_0:25;
assume x in ['(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m)))'] ; :: thesis: abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2
then A42: x in [.(min x0,(x0 + (h . m))),(max x0,(x0 + (h . m))).] by A41, 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 A42, RCOMP_1:def 1;
then A43: ex z being Real st
( x = z & x0 <= z & z <= x0 + (h . m) ) ;
then 0 <= x - x0 by XREAL_1:50;
then A44: abs (x - x0) = x - x0 by ABSVALUE:def 1;
A45: x - x0 <= (x0 + (h . m)) - x0 by A43, XREAL_1:11;
then 0 <= h . m by A43, XREAL_1:50;
hence abs (x - x0) <= abs (h . m) by A45, A44, ABSVALUE:def 1; :: thesis: verum

end;

suppose A46: 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 A42, RCOMP_1:def 1;
then A47: ex z being Real st
( x = z & x0 + (h . m) <= z & z <= x0 ) ;
then A48: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:11;

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

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

(x0 + (h . m)) - x0 < x0 - x0 by A46, XREAL_1:16;
then A50: abs (h . m) = - (h . m) by ABSVALUE:def 1;
x - x0 < 0 by A47, A49, XREAL_1:49;
then abs (x - x0) = - (x - x0) by ABSVALUE:def 1;
hence abs (x - x0) <= abs (h . m) by A48, A50, 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 A51: abs (x - x0) < min (p / 2),(q / 2) by A30, XXREAL_0:2;
then x in ].(x0 - (min (p / 2),(q / 2))),(x0 + (min (p / 2),(q / 2))).[ by RCOMP_1:8;
then x in ].(x0 - q),(x0 + q).[ by A29;
then x in ].a,b.[ by A24, A26;
then A52: x in [.a,b.] by A37;
abs (x - x0) < p / 2 by A39, A51, XXREAL_0:2;
then abs (x - x0) < p by A23, XXREAL_0:2;
then abs ((f . x) - (f . x0)) <= e0 / 2 by A4, A15, A21, A52;
then abs ((f . x1) - ((REAL --> (f . x0)) . x1)) <= e0 / 2 by FUNCOP_1:13;
hence abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 by A15, A36, A52, VALUED_1:13; :: thesis: verum

end;

A53: for x being real number st x in ['a,b'] holds
(REAL --> (f . x0)) . x = f . x0 by FUNCOP_1:13;
then A54: (REAL --> (f . x0)) | ['a,b'] is bounded by A1, A35, Th26;
then A55: (f - (REAL --> (f . x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, RFUNCT_1:101;
rng h c= dom R by A10;
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 A56: (R . (h . m)) / (h . m) = ((h " ) (#) (R /* h)) . m by SEQ_1:12;
h is non-empty by FDIFF_1:def 1;
then h . m <> 0 by SEQ_1:6;
then A57: 0 < abs (h . m) by COMPLEX1:133;
A58: REAL --> (f . x0) is_integrable_on ['a,b'] by A1, A35, A53, Th26;
then f - (REAL --> (f . x0)) is_integrable_on ['a,b'] by A2, A3, A4, A35, A54, Th11;
then A59: abs (integral (f - (REAL --> (f . x0))),x0,(x0 + (h . m))) <= (e0 / 2) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A37, A32, A55, A36, A40, Lm8;
integral (REAL --> (f . x0)),x0,(x0 + (h . m)) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A7, A15, A37, A32, A35, A53, Th27;
then R . (h . m) = integral (f - (REAL --> (f . x0))),x0,(x0 + (h . m)) by A1, A2, A3, A4, A7, A15, A37, A32, A34, A35, A58, A54, A38, Th24;
then ( abs ((R . (h . m)) / (h . m)) = (abs (R . (h . m))) / (abs (h . m)) & (abs (R . (h . m))) / (abs (h . m)) <= ((e0 / 2) * (abs (h . m))) / (abs (h . m)) ) by A59, A57, COMPLEX1:153, XREAL_1:74;
then A60: abs ((R . (h . m)) / (h . m)) <= e0 / 2 by A57, XCMPLX_1:90;
e0 / 2 < e0 by A19, XREAL_1:218;
hence abs ((((h " ) (#) (R /* h)) . m) - 0 ) < e0 by A60, A56, 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 A17, SEQ_2:def 7; :: thesis: verum

end;

consider N being Neighbourhood of x0 such that
A61: N c= ].a,b.[ by A7, RCOMP_1:39;
reconsider R = R as REST by A14, A16, FDIFF_1:def 3;
A62: 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 x in N ; :: thesis: (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))
then x0 + (x - x0) in N ;
then x0 + (R_id (x - x0)) in N by RSSPACE:def 3;
then ( x0 + (R_id (x - x0)) = x0 + (x - x0) & R . (x - x0) = H₃(x - x0) ) by A10, A61, RSSPACE:def 3;
hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ; :: thesis: verum

end;

A63: N c= dom F by A5, A61, XBOOLE_1:1;
hence A64: F is_differentiable_in x0 by A62, FDIFF_1:def 5; :: thesis: diff F,x0 = f . x0
L . 1 = (f . x0) * 1 by A9;
hence diff F,x0 = f . x0 by A63, A62, A64, FDIFF_1:def 6; :: thesis: verum