let a, b, x0 be real number ; :: thesis: for n being non empty 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 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 n be non empty 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 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, 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 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 ) )
deffunc H₁( set ) -> 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 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 the carrier of (REAL-NS n) = $1 * (f /. x0);
consider L being Function of REAL,(REAL-NS n) such that
A9: for h being Real holds L . h = H₂(h) from FUNCT_2:sch 4();
reconsider L = L as LinearFunc of (REAL-NS n) by A9, NDIFF_3:def 2;
deffunc H₃( set ) -> Element of the carrier of (REAL-NS n) = ((F /. (x0 + (R_id $1))) - (F /. x0)) - (L . (R_id $1));
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= the carrier of (REAL-NS n)

proof

let y be set ; :: 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 set such that
A11: x in dom R and
A12: y = R . x by FUNCT_1:def 3;
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 the carrier of (REAL-NS n) by A12, A13; :: thesis: verum

end;

then reconsider R = R as PartFunc of REAL,(REAL-NS n) by A10, RELSET_1:4;
A14: R is total by A10, PARTFUN1:def 2;
A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A16: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) )

proof

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);
A17: for e being Real st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e

proof

set g = REAL --> (f /. x0);
let e0 be Real; :: thesis: ( 0 < e0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 )
set e = (e0 / 2) / n;
A18: ( h is convergent & lim h = 0 ) ;
assume A19: 0 < e0 ; :: thesis: ex n being Element of NAT st
for m being Element of 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 number such that
A20: 0 < p and
A21: for t being real number st t in dom f & abs (t - x0) < p holds
||.((f /. t) - (f /. x0)).|| < (e0 / 2) / n by A8, NFCONT_3:8;
A22: 0 < p / 2 by A20, XREAL_1:215;
A23: p / 2 < p by A20, 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 number such that
A25: 0 < q and
A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def 6;
A27: q / 2 < q by A25, XREAL_1:216;
set r = min ((p / 2),(q / 2));
0 < q / 2 by A25, XREAL_1:215;
then 0 < min ((p / 2),(q / 2)) by A22, XXREAL_0:15;
then consider n0 being Element of NAT such that
A28: for m being Element of NAT st n0 <= m holds
abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A18, SEQ_2:def 7;
take n0 ; :: thesis: for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0
let m be Element of 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 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. (REAL-NS n))).|| < 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:1;
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 A33: R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (h . m)) by RSSPACE:def 3;
A34: 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 A32, A5, PARTFUN1:def 6
.= integral (f,a,(x0 + (h . m))) by A6, A24, A26, A31 ;
then A35: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((h . m) * (f /. x0)) by A34, A9, A33;
A36: 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 A37: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def 2;
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, A15, A32, Th53;
A40: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17;
A41: for x being real number st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds
||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n

proof

let x be real number ; :: thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n )
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) / n
then A43: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def 3, 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 A44: ex z being Real st
( x = z & x0 <= z & z <= x0 + (h . m) ) by A43;
then 0 <= x - x0 by XREAL_1:48;
then A45: abs (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 abs (x - x0) <= abs (h . m) by A46, A45, ABSVALUE:def 1; :: thesis: verum

end;

suppose A47: 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 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 ) ;

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

(x0 + (h . m)) - x0 < x0 - x0 by A47, XREAL_1:14;
then A51: abs (h . m) = - (h . m) by ABSVALUE:def 1;
x - x0 < 0 by A48, A50, XREAL_1:47;
then abs (x - x0) = - (x - x0) by ABSVALUE:def 1;
hence abs (x - x0) <= abs (h . m) by A49, A51, XREAL_1:24; :: 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:46; :: thesis: verum

end;

end;

end;

end;

end;

then A52: 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:1;
then x in ].(x0 - q),(x0 + q).[ by A29;
then x in ].a,b.[ by A24, A26;
then A53: x in [.a,b.] by A38;
reconsider xx = x as Real by XREAL_0:def 1;
abs (x - x0) < p / 2 by A40, A52, XXREAL_0:2;
then abs (x - x0) < p by A23, XXREAL_0:2;
then ||.((f /. x) - (f /. x0)).|| <= (e0 / 2) / n by A4, A15, A21, A53;
then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= (e0 / 2) / n by FUNCOP_1:7;
hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n by A15, A37, A53, VFUNCT_1:def 2; :: thesis: verum

end;

A54: for x being real number st x in ['a,b'] holds
(REAL --> (f /. x0)) . x = f /. x0 by FUNCOP_1:7;
then A55: (REAL --> (f /. x0)) | ['a,b'] is bounded by A1, A36, Th51;
then A56: (f - (REAL --> (f /. x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, Th35;
rng h c= dom R by A10;
then ((h . m) ") * (R /. (h . m)) = ((h . m) ") * ((R /* h) . m) by FUNCT_2:109;
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;
dom h = NAT by FUNCT_2:def 1;
then h . m <> 0 ;
then A58: 0 < abs (h . m) by COMPLEX1:47;
A59: REAL --> (f /. x0) is_integrable_on ['a,b'] by A1, A36, A54, Th51;
then A60: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (n * ((e0 / 2) / n)) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A38, A32, A56, A37, A41, Th54, A2, A4, A36, INTEGR18:15;
A61: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, A15, A38, A32, A36, A54, Th52
.= (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, A2, A3, A4, A7, A15, A38, A32, A36, A59, A55, Th50;
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. (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 A61, RLVECT_1:def 4 ;
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)).|| / (abs (h . m)) & ||.(R /. (h . m)).|| / (abs (h . m)) <= ((n * ((e0 / 2) / n)) * (abs (h . m))) / (abs (h . m)) ) by A60, A58, Lm17, XREAL_1:72;
then ||.(((h . m) ") * (R /. (h . m))).|| <= n * ((e0 / 2) / n) by A58, XCMPLX_1:89;
then A63: ||.(((h . m) ") * (R /. (h . m))).|| <= e0 / 2 by XCMPLX_1:87;
e0 / 2 < e0 by A19, XREAL_1:216;
then ||.(((h ") (#) (R /* h)) . m).|| < e0 by A63, A57, XXREAL_0:2;
hence ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 by RLVECT_1:13; :: thesis: verum

end;

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

end;

consider N being Neighbourhood of x0 such that
A64: N c= ].a,b.[ by A7, RCOMP_1:18;
reconsider R = R as RestFunc of (REAL-NS n) 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

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, A64, RSSPACE:def 3;
then R /. (x - x0) = ((F /. x) - (F /. x0)) - (L . (x - x0)) 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
.= ((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;

A66: N c= dom F by A5, A64, XBOOLE_1:1;
hence A67: F is_differentiable_in x0 by A65, NDIFF_3:def 3; :: thesis: diff (F,x0) = f /. x0
reconsider N1 = 1 as Real ;
L . 1 = N1 * (f /. x0) by A9
.= f /. x0 by RLVECT_1:def 8 ;
hence diff (F,x0) = f /. x0 by A66, A65, A67, NDIFF_3:def 4; :: thesis: verum