let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL

for x0 being Real

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 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

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 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_{1}( object ) -> Element of NAT = 0 ;

let x0 be Real; :: 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 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 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 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_{1}[ object ] means x0 + (In ($1,REAL)) in ].a,b.[;

deffunc H_{2}( Real) -> Element of REAL = In (((f . x0) * $1),REAL);

consider L being Function of REAL,REAL such that

A9: for h being Element of REAL holds L . h = H_{2}(h)
from FUNCT_2:sch 4();

A10: for h being Real holds L . h = (f . x0) * h

deffunc H_{3}( object ) -> set = ((F . (x0 + (In ($1,REAL)))) - (F . x0)) - (L . (In ($1,REAL)));

reconsider L = L as LinearFunc by A10, FDIFF_1:def 3;

consider R being Function such that

A11: ( dom R = REAL & ( for x being object st x in REAL holds

( ( S_{1}[x] implies R . x = H_{3}(x) ) & ( not S_{1}[x] implies R . x = H_{1}(x) ) ) ) )
from PARTFUN1:sch 1();

rng R c= REAL

A15: R is total by A11, PARTFUN1:def 2;

A16: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

A17: for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )

A64: N c= ].a,b.[ by A7, RCOMP_1:18;

reconsider R = R as RestFunc by A15, A17, FDIFF_1:def 2;

A65: for x being Real st x in N holds

(F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))

hence A69: F is_differentiable_in x0 by A65, FDIFF_1:def 4; :: thesis: diff (F,x0) = f . x0

L . 1 = (f . x0) * 1 by A10;

hence diff (F,x0) = f . x0 by A68, A65, A69, FDIFF_1:def 5; :: thesis: verum

for x0 being Real

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 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

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 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

let x0 be Real; :: 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 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 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 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

deffunc H

consider L being Function of REAL,REAL such that

A9: for h being Element of REAL holds L . h = H

A10: for h being Real holds L . h = (f . x0) * h

proof

reconsider L = L as PartFunc of REAL,REAL ;
let h be Real; :: thesis: L . h = (f . x0) * h

reconsider h = h as Element of REAL by XREAL_0:def 1;

L . h = H_{2}(h)
by A9;

hence L . h = (f . x0) * h ; :: thesis: verum

end;reconsider h = h as Element of REAL by XREAL_0:def 1;

L . h = H

hence L . h = (f . x0) * h ; :: thesis: verum

deffunc H

reconsider L = L as LinearFunc by A10, FDIFF_1:def 3;

consider R being Function such that

A11: ( dom R = REAL & ( for x being object st x in REAL holds

( ( S

rng R c= REAL

proof

then reconsider R = R as PartFunc of REAL,REAL by A11, RELSET_1:4;
let y be object ; :: 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 object such that

A12: x in dom R and

A13: y = R . x by FUNCT_1:def 3;

A14: ( not S_{1}[x] implies R . x = H_{1}(x) )
by A11, A12;

( S_{1}[x] implies R . x = H_{3}(x) )
by A11, A12;

hence y in REAL by A13, A14, XREAL_0:def 1; :: thesis: verum

end;assume y in rng R ; :: thesis: y in REAL

then consider x being object such that

A12: x in dom R and

A13: y = R . x by FUNCT_1:def 3;

A14: ( not S

( S

hence y in REAL by A13, A14, XREAL_0:def 1; :: thesis: verum

A15: R is total by A11, PARTFUN1:def 2;

A16: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

A17: for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )

proof

consider N being Neighbourhood of x0 such that
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )

A18: for e being Real st 0 < e holds

ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e

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

end;A18: for e being Real st 0 < e holds

ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e

proof

hence
(h ") (#) (R /* h) is convergent
by SEQ_2:def 6; :: thesis: lim ((h ") (#) (R /* h)) = 0
reconsider fx0 = f . x0 as Element of REAL by XREAL_0:def 1;

set g = REAL --> fx0;

let e0 be Real; :: thesis: ( 0 < e0 implies ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0 )

set e = e0 / 2;

A19: ( h is convergent & lim h = 0 ) ;

assume A20: 0 < e0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0

then 0 < e0 / 2 by XREAL_1:215;

then consider p being Real such that

A21: 0 < p and

A22: for t being Real st t in dom f & |.(t - x0).| < p holds

|.((f . t) - (f . x0)).| < e0 / 2 by A8, FCONT_1:3;

A23: 0 < p / 2 by A21, XREAL_1:215;

A24: p / 2 < p by A21, XREAL_1:216;

consider N being Neighbourhood of x0 such that

A25: N c= ].a,b.[ by A7, RCOMP_1:18;

consider q being Real such that

A26: 0 < q and

A27: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def 6;

A28: q / 2 < q by A26, XREAL_1:216;

set r = min ((p / 2),(q / 2));

0 < q / 2 by A26, XREAL_1:215;

then 0 < min ((p / 2),(q / 2)) by A23, XXREAL_0:15;

then consider n being Nat such that

A29: for m being Nat st n <= m holds

|.((h . m) - 0).| < min ((p / 2),(q / 2)) by A19, SEQ_2:def 7;

take n ; :: thesis: for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (R /* h)) . m) - 0).| < e0 )

min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17;

then A30: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A28, Th2, XXREAL_0:2;

assume n <= m ; :: thesis: |.((((h ") (#) (R /* h)) . m) - 0).| < e0

then A31: |.((h . m) - 0).| < min ((p / 2),(q / 2)) by A29;

then |.((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:1;

then A32: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A30;

then A33: x0 + (h . m) in ].a,b.[ by A25, A27;

then x0 + (In ((h . m),REAL)) in ].a,b.[ ;

then R . (h . m) = ((F . (x0 + (In ((h . m),REAL)))) - (F . x0)) - (L . (In ((h . m),REAL))) by A11;

then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (In ((h . m),REAL))) ;

then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)) ;

then A34: R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A10;

F . (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) by A6, A25, A27, A32;

then A35: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((f . x0) * (h . m)) by A6, A7, A34;

A36: dom (REAL --> fx0) = REAL by FUNCT_2:def 1;

then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> fx0)) by A4, XBOOLE_1:27;

then A37: ['a,b'] c= dom (f - (REAL --> fx0)) by VALUED_1:12;

A38: ].a,b.[ c= [.a,b.] by XXREAL_1:25;

then A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A16, A33, Th20;

A40: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17;

A41: for x being Real st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds

|.((f - (REAL --> fx0)) . x).| <= e0 / 2

(REAL --> fx0) . x = f . x0 by FUNCOP_1:7;

then A56: (REAL --> fx0) | ['a,b'] is bounded by A1, A36, Th26;

then A57: (f - (REAL --> fx0)) | (['a,b'] /\ ['a,b']) is bounded by A3, RFUNCT_1:84;

A58: m in NAT by ORDINAL1:def 12;

rng h c= dom R by A11;

then (R . (h . m)) / (h . m) = ((R /* h) . m) / (h . m) by FUNCT_2:108, A58;

then (R . (h . m)) / (h . m) = ((R /* h) . m) * ((h ") . m) by VALUED_1:10;

then A59: (R . (h . m)) / (h . m) = ((h ") (#) (R /* h)) . m by SEQ_1:8;

h . m <> 0 by SEQ_1:4, A58;

then A60: 0 < |.(h . m).| by COMPLEX1:47;

A61: REAL --> fx0 is_integrable_on ['a,b'] by A1, A36, A55, Th26;

then f - (REAL --> fx0) is_integrable_on ['a,b'] by A2, A3, A4, A36, A56, Th11;

then A62: |.(integral ((f - (REAL --> fx0)),x0,(x0 + (h . m)))).| <= (e0 / 2) * |.((x0 + (h . m)) - x0).| by A1, A7, A16, A38, A33, A57, A37, A41, Lm8;

integral ((REAL --> fx0),x0,(x0 + (h . m))) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A7, A16, A38, A33, A36, A55, Th27;

then R . (h . m) = integral ((f - (REAL --> fx0)),x0,(x0 + (h . m))) by A1, A2, A3, A4, A7, A16, A38, A33, A35, A36, A61, A56, A39, Th24;

then ( |.((R . (h . m)) / (h . m)).| = |.(R . (h . m)).| / |.(h . m).| & |.(R . (h . m)).| / |.(h . m).| <= ((e0 / 2) * |.(h . m).|) / |.(h . m).| ) by A62, A60, COMPLEX1:67, XREAL_1:72;

then A63: |.((R . (h . m)) / (h . m)).| <= e0 / 2 by A60, XCMPLX_1:89;

e0 / 2 < e0 by A20, XREAL_1:216;

hence |.((((h ") (#) (R /* h)) . m) - 0).| < e0 by A63, A59, XXREAL_0:2; :: thesis: verum

end;set g = REAL --> fx0;

let e0 be Real; :: thesis: ( 0 < e0 implies ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0 )

set e = e0 / 2;

A19: ( h is convergent & lim h = 0 ) ;

assume A20: 0 < e0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0

then 0 < e0 / 2 by XREAL_1:215;

then consider p being Real such that

A21: 0 < p and

A22: for t being Real st t in dom f & |.(t - x0).| < p holds

|.((f . t) - (f . x0)).| < e0 / 2 by A8, FCONT_1:3;

A23: 0 < p / 2 by A21, XREAL_1:215;

A24: p / 2 < p by A21, XREAL_1:216;

consider N being Neighbourhood of x0 such that

A25: N c= ].a,b.[ by A7, RCOMP_1:18;

consider q being Real such that

A26: 0 < q and

A27: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def 6;

A28: q / 2 < q by A26, XREAL_1:216;

set r = min ((p / 2),(q / 2));

0 < q / 2 by A26, XREAL_1:215;

then 0 < min ((p / 2),(q / 2)) by A23, XXREAL_0:15;

then consider n being Nat such that

A29: for m being Nat st n <= m holds

|.((h . m) - 0).| < min ((p / 2),(q / 2)) by A19, SEQ_2:def 7;

take n ; :: thesis: for m being Nat st n <= m holds

|.((((h ") (#) (R /* h)) . m) - 0).| < e0

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (R /* h)) . m) - 0).| < e0 )

min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17;

then A30: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A28, Th2, XXREAL_0:2;

assume n <= m ; :: thesis: |.((((h ") (#) (R /* h)) . m) - 0).| < e0

then A31: |.((h . m) - 0).| < min ((p / 2),(q / 2)) by A29;

then |.((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:1;

then A32: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A30;

then A33: x0 + (h . m) in ].a,b.[ by A25, A27;

then x0 + (In ((h . m),REAL)) in ].a,b.[ ;

then R . (h . m) = ((F . (x0 + (In ((h . m),REAL)))) - (F . x0)) - (L . (In ((h . m),REAL))) by A11;

then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (In ((h . m),REAL))) ;

then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)) ;

then A34: R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A10;

F . (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) by A6, A25, A27, A32;

then A35: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((f . x0) * (h . m)) by A6, A7, A34;

A36: dom (REAL --> fx0) = REAL by FUNCT_2:def 1;

then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> fx0)) by A4, XBOOLE_1:27;

then A37: ['a,b'] c= dom (f - (REAL --> fx0)) by VALUED_1:12;

A38: ].a,b.[ c= [.a,b.] by XXREAL_1:25;

then A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A16, A33, Th20;

A40: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17;

A41: for x being Real st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds

|.((f - (REAL --> fx0)) . x).| <= e0 / 2

proof

A55:
for x being Real st x in ['a,b'] holds
let x be Real; :: thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies |.((f - (REAL --> fx0)) . x).| <= e0 / 2 )

reconsider x1 = x as Real ;

A42: ( 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: |.((f - (REAL --> fx0)) . x).| <= e0 / 2

then A43: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def 3, XXREAL_0:2;

|.(x - x0).| <= |.(h . m).|

then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;

then x in ].(x0 - q),(x0 + q).[ by A30;

then x in ].a,b.[ by A25, A27;

then A53: x in [.a,b.] by A38;

A54: x1 in REAL by XREAL_0:def 1;

|.(x - x0).| < p / 2 by A40, A52, XXREAL_0:2;

then |.(x - x0).| < p by A24, XXREAL_0:2;

then |.((f . x) - (f . x0)).| <= e0 / 2 by A4, A16, A22, A53;

then |.((f . x1) - ((REAL --> fx0) . x1)).| <= e0 / 2 by FUNCOP_1:7, A54;

hence |.((f - (REAL --> fx0)) . x).| <= e0 / 2 by A16, A37, A53, VALUED_1:13; :: thesis: verum

end;reconsider x1 = x as Real ;

A42: ( 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: |.((f - (REAL --> fx0)) . x).| <= e0 / 2

then A43: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def 3, XXREAL_0:2;

|.(x - x0).| <= |.(h . m).|

proof
end;

then A52:
|.(x - x0).| < min ((p / 2),(q / 2))
by A31, XXREAL_0:2;per cases
( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) )
;

end;

suppose
x0 <= x0 + (h . m)
; :: thesis: |.(x - x0).| <= |.(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 A43, RCOMP_1:def 1;

then A44: ex z being Real st

( x = z & x0 <= z & z <= x0 + (h . m) ) ;

then 0 <= x - x0 by XREAL_1:48;

then A45: |.(x - x0).| = x - x0 by ABSVALUE:def 1;

A46: x - x0 <= (x0 + (h . m)) - x0 by A44, XREAL_1:9;

then 0 <= h . m by A44, XREAL_1:48;

hence |.(x - x0).| <= |.(h . m).| by A46, A45, ABSVALUE:def 1; :: thesis: verum

end;then x in { z where z is Real : ( x0 <= z & z <= x0 + (h . m) ) } by A43, RCOMP_1:def 1;

then A44: ex z being Real st

( x = z & x0 <= z & z <= x0 + (h . m) ) ;

then 0 <= x - x0 by XREAL_1:48;

then A45: |.(x - x0).| = x - x0 by ABSVALUE:def 1;

A46: x - x0 <= (x0 + (h . m)) - x0 by A44, XREAL_1:9;

then 0 <= h . m by A44, XREAL_1:48;

hence |.(x - x0).| <= |.(h . m).| by A46, A45, ABSVALUE:def 1; :: thesis: verum

suppose A47:
not x0 <= x0 + (h . m)
; :: thesis: |.(x - x0).| <= |.(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 A43, RCOMP_1:def 1;

then A48: ex z being Real st

( x = z & x0 + (h . m) <= z & z <= x0 ) ;

then A49: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9;

end;then x in { z where z is Real : ( x0 + (h . m) <= z & z <= x0 ) } by A43, RCOMP_1:def 1;

then A48: ex z being Real st

( x = z & x0 + (h . m) <= z & z <= x0 ) ;

then A49: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9;

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

end;

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

(x0 + (h . m)) - x0 < x0 - x0
by A47, XREAL_1:14;

then A51: |.(h . m).| = - (h . m) by ABSVALUE:def 1;

x - x0 < 0 by A48, A50, XREAL_1:47;

then |.(x - x0).| = - (x - x0) by ABSVALUE:def 1;

hence |.(x - x0).| <= |.(h . m).| by A49, A51, XREAL_1:24; :: thesis: verum

end;then A51: |.(h . m).| = - (h . m) by ABSVALUE:def 1;

x - x0 < 0 by A48, A50, XREAL_1:47;

then |.(x - x0).| = - (x - x0) by ABSVALUE:def 1;

hence |.(x - x0).| <= |.(h . m).| by A49, A51, XREAL_1:24; :: thesis: verum

then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;

then x in ].(x0 - q),(x0 + q).[ by A30;

then x in ].a,b.[ by A25, A27;

then A53: x in [.a,b.] by A38;

A54: x1 in REAL by XREAL_0:def 1;

|.(x - x0).| < p / 2 by A40, A52, XXREAL_0:2;

then |.(x - x0).| < p by A24, XXREAL_0:2;

then |.((f . x) - (f . x0)).| <= e0 / 2 by A4, A16, A22, A53;

then |.((f . x1) - ((REAL --> fx0) . x1)).| <= e0 / 2 by FUNCOP_1:7, A54;

hence |.((f - (REAL --> fx0)) . x).| <= e0 / 2 by A16, A37, A53, VALUED_1:13; :: thesis: verum

(REAL --> fx0) . x = f . x0 by FUNCOP_1:7;

then A56: (REAL --> fx0) | ['a,b'] is bounded by A1, A36, Th26;

then A57: (f - (REAL --> fx0)) | (['a,b'] /\ ['a,b']) is bounded by A3, RFUNCT_1:84;

A58: m in NAT by ORDINAL1:def 12;

rng h c= dom R by A11;

then (R . (h . m)) / (h . m) = ((R /* h) . m) / (h . m) by FUNCT_2:108, A58;

then (R . (h . m)) / (h . m) = ((R /* h) . m) * ((h ") . m) by VALUED_1:10;

then A59: (R . (h . m)) / (h . m) = ((h ") (#) (R /* h)) . m by SEQ_1:8;

h . m <> 0 by SEQ_1:4, A58;

then A60: 0 < |.(h . m).| by COMPLEX1:47;

A61: REAL --> fx0 is_integrable_on ['a,b'] by A1, A36, A55, Th26;

then f - (REAL --> fx0) is_integrable_on ['a,b'] by A2, A3, A4, A36, A56, Th11;

then A62: |.(integral ((f - (REAL --> fx0)),x0,(x0 + (h . m)))).| <= (e0 / 2) * |.((x0 + (h . m)) - x0).| by A1, A7, A16, A38, A33, A57, A37, A41, Lm8;

integral ((REAL --> fx0),x0,(x0 + (h . m))) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A7, A16, A38, A33, A36, A55, Th27;

then R . (h . m) = integral ((f - (REAL --> fx0)),x0,(x0 + (h . m))) by A1, A2, A3, A4, A7, A16, A38, A33, A35, A36, A61, A56, A39, Th24;

then ( |.((R . (h . m)) / (h . m)).| = |.(R . (h . m)).| / |.(h . m).| & |.(R . (h . m)).| / |.(h . m).| <= ((e0 / 2) * |.(h . m).|) / |.(h . m).| ) by A62, A60, COMPLEX1:67, XREAL_1:72;

then A63: |.((R . (h . m)) / (h . m)).| <= e0 / 2 by A60, XCMPLX_1:89;

e0 / 2 < e0 by A20, XREAL_1:216;

hence |.((((h ") (#) (R /* h)) . m) - 0).| < e0 by A63, A59, XXREAL_0:2; :: thesis: verum

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

A64: N c= ].a,b.[ by A7, RCOMP_1:18;

reconsider R = R as RestFunc by A15, A17, FDIFF_1:def 2;

A65: for x being Real st x in N holds

(F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))

proof

A68:
N c= dom F
by A5, A64;
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 A66: x0 + (x - x0) in N ;

reconsider x = x as Real ;

A67: x0 + (x - x0) in N by A66;

S_{1}[x - x0]
by A67, A64;

then R . (x - x0) = H_{3}(x - x0)
by A11;

hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ; :: thesis: verum

end;assume x in N ; :: thesis: (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))

then A66: x0 + (x - x0) in N ;

reconsider x = x as Real ;

A67: x0 + (x - x0) in N by A66;

S

then R . (x - x0) = H

hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ; :: thesis: verum

hence A69: F is_differentiable_in x0 by A65, FDIFF_1:def 4; :: thesis: diff (F,x0) = f . x0

L . 1 = (f . x0) * 1 by A10;

hence diff (F,x0) = f . x0 by A68, A65, A69, FDIFF_1:def 5; :: thesis: verum