let a, b, x0 be Real; :: thesis: for n being non zero Element of NAT

for F, f being PartFunc of REAL,(REAL-NS n) 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 n be non zero Element of NAT ; :: thesis: for F, f being PartFunc of REAL,(REAL-NS n) 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, f be PartFunc of REAL,(REAL-NS n); :: 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 ) )

deffunc H_{1}( object ) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n);

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 the carrier of (REAL-NS n) = $1 * (f /. x0);

consider L being Function of REAL,(REAL-NS n) 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 = H_{2}(h)
_{2}(h)

deffunc H_{3}( object ) -> Element of the carrier of (REAL-NS n) = ((F /. (x0 + (In ($1,REAL)))) - (F /. x0)) - (L . (In ($1,REAL)));

consider R being Function such that

A12: ( 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= the carrier of (REAL-NS n)

A16: R is total by A12, PARTFUN1:def 2;

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

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

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) )

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

reconsider R = R as RestFunc of (REAL-NS n) by A16, A18, NDIFF_3:def 1;

A68: for x being Real st x in N holds

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

hence A73: F is_differentiable_in x0 by A68, NDIFF_3:def 3; :: thesis: diff (F,x0) = f /. x0

reconsider N1 = 1 as Real ;

L /. 1 = N1 * (f /. x0) by A11

.= f /. x0 by RLVECT_1:def 8 ;

hence diff (F,x0) = f /. x0 by A72, A68, A73, NDIFF_3:def 4; :: thesis: verum

for F, f being PartFunc of REAL,(REAL-NS n) 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 n be non zero Element of NAT ; :: thesis: for F, f being PartFunc of REAL,(REAL-NS n) 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, f be PartFunc of REAL,(REAL-NS n); :: 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 ) )

deffunc H

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-NS n) such that

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

A10: for h being Real holds L . h = H

proof

A11:
for h being Real holds L /. h = H
let h be Real; :: thesis: L . h = H_{2}(h)

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

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

hence L . h = H_{2}(h)
; :: thesis: verum

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

L . h = H

hence L . h = H

proof

then reconsider L = L as LinearFunc of (REAL-NS n) by NDIFF_3:def 2;
let h be Real; :: thesis: L /. h = H_{2}(h)

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

L /. h = L . h

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

hence L /. h = H_{2}(h)
; :: thesis: verum

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

L /. h = L . h

.= H

hence L /. h = H

deffunc H

consider R being Function such that

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

( ( S

rng R c= the carrier of (REAL-NS n)

proof

then reconsider R = R as PartFunc of REAL,(REAL-NS n) by A12, RELSET_1:4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng R or y in the carrier of (REAL-NS n) )

assume y in rng R ; :: thesis: y in the carrier of (REAL-NS n)

then consider x being object such that

A13: x in dom R and

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

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

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

hence y in the carrier of (REAL-NS n) by A14, A15; :: thesis: verum

end;assume y in rng R ; :: thesis: y in the carrier of (REAL-NS n)

then consider x being object such that

A13: x in dom R and

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

A15: ( not S

( S

hence y in the carrier of (REAL-NS n) by A14, A15; :: thesis: verum

A16: R is total by A12, PARTFUN1:def 2;

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

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

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) )

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. (REAL-NS n) )

set Z0 = 0. (REAL-NS n);

A19: 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. (REAL-NS n))).|| < e

hence lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) by A19, NORMSP_1:def 7; :: thesis: verum

end;set Z0 = 0. (REAL-NS n);

A19: 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. (REAL-NS n))).|| < e

proof

hence
(h ") (#) (R /* h) is convergent
by NORMSP_1:def 6; :: thesis: lim ((h ") (#) (R /* h)) = 0. (REAL-NS n)
set g = REAL --> (f /. x0);

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. (REAL-NS n))).|| < e0 )

set e = (e0 / 2) / n;

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

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

for m being Nat st n <= m holds

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

then 0 < e0 / 2 by XREAL_1:215;

then 0 < (e0 / 2) / n by XREAL_1:139;

then consider p being Real such that

A22: 0 < p and

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

||.((f /. t) - (f /. x0)).|| < (e0 / 2) / n by A8, NFCONT_3:8;

A24: 0 < p / 2 by A22, XREAL_1:215;

A25: p / 2 < p by A22, XREAL_1:216;

consider N being Neighbourhood of x0 such that

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

consider q being Real such that

A27: 0 < q and

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

A29: q / 2 < q by A27, XREAL_1:216;

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

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

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

then consider n0 being Nat such that

A30: for m being Nat st n0 <= m holds

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

reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;

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

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

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

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

then A31: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A29, INTEGRA6:2, XXREAL_0:2;

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

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

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 A33: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A31;

then A34: x0 + (h . m) in ].a,b.[ by A26, A28;

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

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

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

A36: F /. x0 = F . x0 by A7, A5, PARTFUN1:def 6

.= integral (f,a,x0) by A6, A7 ;

F /. (x0 + (h . m)) = F . (x0 + (h . m)) by A34, A5, PARTFUN1:def 6

.= integral (f,a,(x0 + (h . m))) by A6, A26, A28, A33 ;

then A37: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((h . m) * (f /. x0)) by A36, A10, A35;

A38: 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 A39: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def 2;

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

then A41: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A17, A34, Th53;

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

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

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

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

then A57: (REAL --> (f /. x0)) | ['a,b'] is bounded by A1, A38, Th51;

then A58: (f - (REAL --> (f /. x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, Th35;

A59: m in NAT by ORDINAL1:def 12;

rng h c= dom R by A12;

then ((h . m) ") * (R /. (h . m)) = ((h . m) ") * ((R /* h) . m) by FUNCT_2:109, A59;

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

then A60: ((h . m) ") * (R /. (h . m)) = ((h ") (#) (R /* h)) . m by NDIFF_1:def 2;

h . m <> 0 by SEQ_1:5;

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

A62: REAL --> (f /. x0) is_integrable_on ['a,b'] by A1, A38, A56, Th51;

then A63: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (n * ((e0 / 2) / n)) * |.((x0 + (h . m)) - x0).| by A1, A7, A17, A40, A34, A58, A39, A43, Th54, A2, A4, A38, INTEGR18:15;

A64: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, A17, A40, A34, A38, A56, Th52

.= (h . m) * (f /. x0) ;

A65: integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) = (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A17, A40, A34, A38, A62, A57, Th50;

R . (h . m) = ((integral (f,x0,(x0 + (h . m)))) + ((integral (f,a,x0)) - (integral (f,a,x0)))) - ((h . m) * (f /. x0)) by A37, A41, RLVECT_1:28

.= ((integral (f,x0,(x0 + (h . m)))) + (0. (REAL-NS n))) - ((h . m) * (f /. x0)) by RLVECT_1:15

.= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A64, RLVECT_1:def 4 ;

then R /. (h . m) = integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) by A65, A12, PARTFUN1:def 6;

then ( ||.(((h . m) ") * (R /. (h . m))).|| = ||.(R /. (h . m)).|| / |.(h . m).| & ||.(R /. (h . m)).|| / |.(h . m).| <= ((n * ((e0 / 2) / n)) * |.(h . m).|) / |.(h . m).| ) by A63, A61, Lm17, XREAL_1:72;

then ||.(((h . m) ") * (R /. (h . m))).|| <= n * ((e0 / 2) / n) by A61, XCMPLX_1:89;

then A66: ||.(((h . m) ") * (R /. (h . m))).|| <= e0 / 2 by XCMPLX_1:87;

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

then ||.(((h ") (#) (R /* h)) . m).|| < e0 by A66, A60, XXREAL_0:2;

hence ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 by RLVECT_1:13; :: thesis: verum

end;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. (REAL-NS n))).|| < e0 )

set e = (e0 / 2) / n;

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

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

for m being Nat st n <= m holds

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

then 0 < e0 / 2 by XREAL_1:215;

then 0 < (e0 / 2) / n by XREAL_1:139;

then consider p being Real such that

A22: 0 < p and

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

||.((f /. t) - (f /. x0)).|| < (e0 / 2) / n by A8, NFCONT_3:8;

A24: 0 < p / 2 by A22, XREAL_1:215;

A25: p / 2 < p by A22, XREAL_1:216;

consider N being Neighbourhood of x0 such that

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

consider q being Real such that

A27: 0 < q and

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

A29: q / 2 < q by A27, XREAL_1:216;

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

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

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

then consider n0 being Nat such that

A30: for m being Nat st n0 <= m holds

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

reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;

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

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

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

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

then A31: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A29, INTEGRA6:2, XXREAL_0:2;

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

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

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 A33: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A31;

then A34: x0 + (h . m) in ].a,b.[ by A26, A28;

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

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

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

A36: F /. x0 = F . x0 by A7, A5, PARTFUN1:def 6

.= integral (f,a,x0) by A6, A7 ;

F /. (x0 + (h . m)) = F . (x0 + (h . m)) by A34, A5, PARTFUN1:def 6

.= integral (f,a,(x0 + (h . m))) by A6, A26, A28, A33 ;

then A37: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((h . m) * (f /. x0)) by A36, A10, A35;

A38: 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 A39: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def 2;

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

then A41: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A17, A34, Th53;

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

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

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

proof

A56:
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 --> (f /. x0))) /. x).|| <= (e0 / 2) / n )

A44: ( 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 --> (f /. x0))) /. x).|| <= (e0 / 2) / n

then A45: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A44, 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 A31;

then x in ].a,b.[ by A26, A28;

then A55: x in [.a,b.] by A40;

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

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

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

then ||.((f /. x) - (f /. x0)).|| <= (e0 / 2) / n by A4, A17, A23, A55;

then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= (e0 / 2) / n by FUNCOP_1:7;

hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n by A17, A39, A55, VFUNCT_1:def 2; :: thesis: verum

end;A44: ( 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 --> (f /. x0))) /. x).|| <= (e0 / 2) / n

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

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

proof
end;

then A54:
|.(x - x0).| < min ((p / 2),(q / 2))
by A32, 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 A46: ex z being Real st

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

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

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

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

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

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

end;then A46: ex z being Real st

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

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

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

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

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

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

suppose A49:
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 A50: ex z being Real st

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

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

end;then A50: ex z being Real st

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

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

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

end;

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

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

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

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

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

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

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

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

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

hence |.(x - x0).| <= |.(h . m).| by A51, A53, 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 A31;

then x in ].a,b.[ by A26, A28;

then A55: x in [.a,b.] by A40;

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

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

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

then ||.((f /. x) - (f /. x0)).|| <= (e0 / 2) / n by A4, A17, A23, A55;

then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= (e0 / 2) / n by FUNCOP_1:7;

hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n by A17, A39, A55, VFUNCT_1:def 2; :: thesis: verum

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

then A57: (REAL --> (f /. x0)) | ['a,b'] is bounded by A1, A38, Th51;

then A58: (f - (REAL --> (f /. x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, Th35;

A59: m in NAT by ORDINAL1:def 12;

rng h c= dom R by A12;

then ((h . m) ") * (R /. (h . m)) = ((h . m) ") * ((R /* h) . m) by FUNCT_2:109, A59;

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

then A60: ((h . m) ") * (R /. (h . m)) = ((h ") (#) (R /* h)) . m by NDIFF_1:def 2;

h . m <> 0 by SEQ_1:5;

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

A62: REAL --> (f /. x0) is_integrable_on ['a,b'] by A1, A38, A56, Th51;

then A63: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (n * ((e0 / 2) / n)) * |.((x0 + (h . m)) - x0).| by A1, A7, A17, A40, A34, A58, A39, A43, Th54, A2, A4, A38, INTEGR18:15;

A64: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, A17, A40, A34, A38, A56, Th52

.= (h . m) * (f /. x0) ;

A65: integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) = (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A17, A40, A34, A38, A62, A57, Th50;

R . (h . m) = ((integral (f,x0,(x0 + (h . m)))) + ((integral (f,a,x0)) - (integral (f,a,x0)))) - ((h . m) * (f /. x0)) by A37, A41, RLVECT_1:28

.= ((integral (f,x0,(x0 + (h . m)))) + (0. (REAL-NS n))) - ((h . m) * (f /. x0)) by RLVECT_1:15

.= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A64, RLVECT_1:def 4 ;

then R /. (h . m) = integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) by A65, A12, PARTFUN1:def 6;

then ( ||.(((h . m) ") * (R /. (h . m))).|| = ||.(R /. (h . m)).|| / |.(h . m).| & ||.(R /. (h . m)).|| / |.(h . m).| <= ((n * ((e0 / 2) / n)) * |.(h . m).|) / |.(h . m).| ) by A63, A61, Lm17, XREAL_1:72;

then ||.(((h . m) ") * (R /. (h . m))).|| <= n * ((e0 / 2) / n) by A61, XCMPLX_1:89;

then A66: ||.(((h . m) ") * (R /. (h . m))).|| <= e0 / 2 by XCMPLX_1:87;

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

then ||.(((h ") (#) (R /* h)) . m).|| < e0 by A66, A60, XXREAL_0:2;

hence ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 by RLVECT_1:13; :: thesis: verum

hence lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) by A19, NORMSP_1:def 7; :: thesis: verum

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

reconsider R = R as RestFunc of (REAL-NS n) by A16, A18, NDIFF_3:def 1;

A68: for x being Real st x in N holds

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

proof

A72:
N c= dom F
by A5, A67;
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 A69: x0 + (In ((x - x0),REAL)) in N ;

then A70: ( x0 + (In ((x - x0),REAL)) = x0 + (x - x0) & R . (x - x0) = H_{3}(x - x0) )
by A12, A67;

x0 + (In ((x - x0),REAL)) in ].a,b.[ by A69, A67;

then A71: S_{1}[x - x0]
;

R /. (x - x0) = R . (x - x0) by A12, PARTFUN1:def 6, A70

.= H_{3}(x - x0)
by A12, A71

.= ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L . (In ((x - x0),REAL)))

.= ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L /. (In ((x - x0),REAL)))

.= ((F /. x) - (F /. x0)) - (L /. (x - x0)) ;

then (R /. (x - x0)) + (L /. (x - x0)) = ((F /. x) - (F /. x0)) - ((L /. (x - x0)) - (L /. (x - x0))) by RLVECT_1:29

.= ((F /. x) - (F /. x0)) - (0. (REAL-NS n)) by RLVECT_1:15

.= (F /. x) - (F /. x0) by RLVECT_1:13 ;

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 x0 + (x - x0) in N ;

then A69: x0 + (In ((x - x0),REAL)) in N ;

then A70: ( x0 + (In ((x - x0),REAL)) = x0 + (x - x0) & R . (x - x0) = H

x0 + (In ((x - x0),REAL)) in ].a,b.[ by A69, A67;

then A71: S

R /. (x - x0) = R . (x - x0) by A12, PARTFUN1:def 6, A70

.= H

.= ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L . (In ((x - x0),REAL)))

.= ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L /. (In ((x - x0),REAL)))

.= ((F /. x) - (F /. x0)) - (L /. (x - x0)) ;

then (R /. (x - x0)) + (L /. (x - x0)) = ((F /. x) - (F /. x0)) - ((L /. (x - x0)) - (L /. (x - x0))) by RLVECT_1:29

.= ((F /. x) - (F /. x0)) - (0. (REAL-NS n)) by RLVECT_1:15

.= (F /. x) - (F /. x0) by RLVECT_1:13 ;

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

hence A73: F is_differentiable_in x0 by A68, NDIFF_3:def 3; :: thesis: diff (F,x0) = f /. x0

reconsider N1 = 1 as Real ;

L /. 1 = N1 * (f /. x0) by A11

.= f /. x0 by RLVECT_1:def 8 ;

hence diff (F,x0) = f /. x0 by A72, A68, A73, NDIFF_3:def 4; :: thesis: verum