let a, b, x0 be Real; :: thesis: for X being RealBanachSpace

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.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 X be RealBanachSpace; :: thesis: for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.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, the carrier of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st [.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 continuous PartFunc of REAL, the carrier of X; :: thesis: ( [.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 X = 0. X;

assume that

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 )

for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.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 X be RealBanachSpace; :: thesis: for F being PartFunc of REAL, the carrier of X

for f being continuous PartFunc of REAL, the carrier of X st [.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, the carrier of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st [.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 continuous PartFunc of REAL, the carrier of X; :: thesis: ( [.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

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 )

per cases
( a <= b or a > b )
;

end;

suppose A1:
a <= b
; :: thesis: ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

then X5:
['a,b'] = [.a,b.]
by INTEGRA5:def 3;

defpred S_{1}[ object ] means x0 + (In ($1,REAL)) in ].a,b.[;

deffunc H_{2}( Real) -> Element of the carrier of X = $1 * (f /. x0);

consider L being Function of REAL, the carrier of X such that

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

A9: for h being Real holds L . h = H_{2}(h)
_{2}(h)

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

consider R being Function such that

A10: ( 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 X

A14: R is total by A10, PARTFUN1:def 2;

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

then X1: ].a,b.[ c= ['a,b'] by XXREAL_1:25;

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

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

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

reconsider R = R as RestFunc of X by A14, A16, NDIFF_3:def 1;

A65: for x being Real st x in N holds

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

hence A67: F is_differentiable_in x0 by A65; :: thesis: diff (F,x0) = f /. x0

reconsider N1 = 1 as Real ;

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

then L /. 1 = f /. x0 by RLVECT_1:def 8;

hence diff (F,x0) = f /. x0 by A66, A65, A67, NDIFF_3:def 4; :: thesis: verum

end;defpred S

deffunc H

consider L being Function of REAL, the carrier of X such that

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

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

proof

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

h is Element of REAL by XREAL_0:def 1;

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

end;h is Element of REAL by XREAL_0:def 1;

hence L . h = H

proof

then reconsider L = L as LinearFunc of X 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 = H_{2}(h)
by B9;

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

deffunc H

consider R being Function such that

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

( ( S

rng R c= the carrier of X

proof

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

assume y in rng R ; :: thesis: y in the carrier of X

then consider x being object such that

A11: ( x in dom R & y = R . x ) by FUNCT_1:def 3;

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

hence y in the carrier of X by A11; :: thesis: verum

end;assume y in rng R ; :: thesis: y in the carrier of X

then consider x being object such that

A11: ( x in dom R & y = R . x ) by FUNCT_1:def 3;

( ( S

hence y in the carrier of X by A11; :: thesis: verum

A14: R is total by A10, PARTFUN1:def 2;

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

then X1: ].a,b.[ c= ['a,b'] by XXREAL_1:25;

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

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

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. X )

set Z0 = 0. X;

A17: 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. X)).|| < e

hence lim ((h ") (#) (R /* h)) = 0. X by A17, NORMSP_1:def 7; :: thesis: verum

end;set Z0 = 0. X;

A17: 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. X)).|| < e

proof

hence
(h ") (#) (R /* h) is convergent
; :: thesis: lim ((h ") (#) (R /* h)) = 0. X
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. X)).|| < e0 )

set e = e0 / 2;

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

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

for m being Nat st n <= m holds

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

then consider p being Real such that

A20: 0 < p and

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

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

A22: ( e0 / 2 < e0 & 0 < p / 2 & p / 2 < p ) by A19, A20, XREAL_1:215, XREAL_1:216;

consider N being Neighbourhood of x0 such that

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

consider q being Real such that

A25: 0 < q and

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

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

A27: ( 0 < q / 2 & q / 2 < q ) by A25, XREAL_1:215, XREAL_1:216;

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

then consider n0 being Nat such that

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

|.((h . m) - 0).| < min ((p / 2),(q / 2)) by A18, 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. X)).|| < e0

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

A40: ( min ((p / 2),(q / 2)) <= p / 2 & 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, INTEGRA6:2, XXREAL_0:2;

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

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

then |.((x0 + (h . m)) - x0).| < min ((p / 2),(q / 2)) ;

then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29, RCOMP_1:1;

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

A32: R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (In ((h . m),REAL))) by A10, A24, A26, A31;

( F /. x0 = integral (f,a,x0) & F /. (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) ) by A6, A7, A24, A26, A31;

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

A36: dom (REAL --> (f /. x0)) = REAL ;

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

then A37: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def 2;

A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, X5, A4, A7, X1, X2, INTEGR21:29;

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

rng h c= dom R by A10;

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

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

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

A58: 0 < |.(h . m).| by COMPLEX1:47, SEQ_1:5;

A60: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (e0 / 2) * |.((x0 + (h . m)) - x0).| by A1, A7, X1, X2, A37, A41, INTEGR21:25;

A61: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, X1, X2, A36, B54, INTEGR21:28

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

A62: 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, X5, A4, A7, X1, X2, A36, INTEGR21:30;

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

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

.= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A61 ;

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

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

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

hence ||.((((h ") (#) (R /* h)) . m) - (0. X)).|| < e0 by A22, A57, XXREAL_0:2; :: 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. X)).|| < e0 )

set e = e0 / 2;

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

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

for m being Nat st n <= m holds

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

then consider p being Real such that

A20: 0 < p and

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

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

A22: ( e0 / 2 < e0 & 0 < p / 2 & p / 2 < p ) by A19, A20, XREAL_1:215, XREAL_1:216;

consider N being Neighbourhood of x0 such that

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

consider q being Real such that

A25: 0 < q and

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

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

A27: ( 0 < q / 2 & q / 2 < q ) by A25, XREAL_1:215, XREAL_1:216;

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

then consider n0 being Nat such that

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

|.((h . m) - 0).| < min ((p / 2),(q / 2)) by A18, 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. X)).|| < e0

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

A40: ( min ((p / 2),(q / 2)) <= p / 2 & 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, INTEGRA6:2, XXREAL_0:2;

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

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

then |.((x0 + (h . m)) - x0).| < min ((p / 2),(q / 2)) ;

then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29, RCOMP_1:1;

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

A32: R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (In ((h . m),REAL))) by A10, A24, A26, A31;

( F /. x0 = integral (f,a,x0) & F /. (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) ) by A6, A7, A24, A26, A31;

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

A36: dom (REAL --> (f /. x0)) = REAL ;

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

then A37: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def 2;

A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, X5, A4, A7, X1, X2, INTEGR21:29;

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

proof

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 )

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 --> (f /. x0))) /. 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 - q),(x0 + q).[ by A29, RCOMP_1:1;

then A53: x in [.a,b.] by X1, A15, A24, A26;

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

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

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

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

then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= e0 / 2 ;

hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= e0 / 2 by A15, A37, A53, VFUNCT_1:def 2; :: thesis: verum

end;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 --> (f /. x0))) /. 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 A30, 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 A44: ex z being Real st

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

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

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 A44: ex z being Real st

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

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

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 A48: ex z being Real st

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

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

end;then A48: ex z being Real st

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

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

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

end;

then x in ].(x0 - q),(x0 + q).[ by A29, RCOMP_1:1;

then A53: x in [.a,b.] by X1, A15, A24, A26;

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

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

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

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

then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= e0 / 2 ;

hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= e0 / 2 by A15, A37, A53, VFUNCT_1:def 2; :: thesis: verum

B54: now :: thesis: for x being Real st x in ['a,b'] holds

(REAL --> (f /. x0)) /. x = f /. x0

XX:
m in NAT
by ORDINAL1:def 12;(REAL --> (f /. x0)) /. x = f /. x0

let x be Real; :: thesis: ( x in ['a,b'] implies (REAL --> (f /. x0)) /. x = f /. x0 )

assume B1: x in ['a,b'] ; :: thesis: (REAL --> (f /. x0)) /. x = f /. x0

thus (REAL --> (f /. x0)) /. x = (REAL --> (f /. x0)) . x by A36, XREAL_0:def 1, PARTFUN1:def 6

.= f /. x0 by B1, FUNCOP_1:7 ; :: thesis: verum

end;assume B1: x in ['a,b'] ; :: thesis: (REAL --> (f /. x0)) /. x = f /. x0

thus (REAL --> (f /. x0)) /. x = (REAL --> (f /. x0)) . x by A36, XREAL_0:def 1, PARTFUN1:def 6

.= f /. x0 by B1, FUNCOP_1:7 ; :: thesis: verum

rng h c= dom R by A10;

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

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

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

A58: 0 < |.(h . m).| by COMPLEX1:47, SEQ_1:5;

A60: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (e0 / 2) * |.((x0 + (h . m)) - x0).| by A1, A7, X1, X2, A37, A41, INTEGR21:25;

A61: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, X1, X2, A36, B54, INTEGR21:28

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

A62: 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, X5, A4, A7, X1, X2, A36, INTEGR21:30;

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

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

.= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A61 ;

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

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

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

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

hence lim ((h ") (#) (R /* h)) = 0. X by A17, NORMSP_1:def 7; :: thesis: verum

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

reconsider R = R as RestFunc of X by A14, A16, NDIFF_3:def 1;

A65: for x being Real st x in N holds

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

proof

A66:
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 ( x0 + (In ((x - x0),REAL)) = x0 + (x - x0) & R . (x - x0) = H_{3}(x - x0) )
by A10, A64;

then R /. (x - x0) = ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L /. (In ((x - x0),REAL))) by A10, PARTFUN1:def 6;

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

then (R /. (x - x0)) + (L /. (x - x0)) = ((F /. x) - (F /. x0)) - (0. X) by RLVECT_1:15;

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 + (In ((x - x0),REAL)) = x0 + (x - x0) & R . (x - x0) = H

then R /. (x - x0) = ((F /. (x0 + (In ((x - x0),REAL)))) - (F /. x0)) - (L /. (In ((x - x0),REAL))) by A10, PARTFUN1:def 6;

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

then (R /. (x - x0)) + (L /. (x - x0)) = ((F /. x) - (F /. x0)) - (0. X) by RLVECT_1:15;

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

hence A67: F is_differentiable_in x0 by A65; :: thesis: diff (F,x0) = f /. x0

reconsider N1 = 1 as Real ;

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

then L /. 1 = f /. x0 by RLVECT_1:def 8;

hence diff (F,x0) = f /. x0 by A66, A65, A67, NDIFF_3:def 4; :: thesis: verum