0; 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 thesis by A49,A51,XREAL_1:24; end; suppose x-x0 = 0; then abs(x-x0) = 0 by ABSVALUE:def 1; hence thesis by COMPLEX1:46; end; end; end; then A52: abs(x-x0) < r by A30,XXREAL_0:2; then x in ].x0-r,x0+r.[ 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 .|| <= e by A4,A15,A21,A53; then ||. f/.x- g/.xx .|| <= e by FUNCOP_1:7; hence thesis by A15,A37,A53,VFUNCT_1:def 2; end; A54: for x be real number st x in ['a,b'] holds g.x = f/.x0 by FUNCOP_1:7; then A55: g| ['a,b'] is bounded by A1,A36,Th52; then A56: (f-g) | (['a,b'] /\ ['a,b']) is bounded by A3,Th36; 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; A58: 0 < abs(h.m) by COMPLEX1:47; A59: g is_integrable_on ['a,b'] by A1,A36,A54,Th52; then A60: ||. integral(f-g,x0,x0+h.m) .|| <= (n*e)*abs(x0+h.m-x0) by A1,A7,A15,A38,A32,A56,A37,A41,Lm16,A2,A4,A36,INTEGR18:15; A61: integral(g,x0,x0+h.m)=((x0+h.m)-x0)*(f/.x0) by A1,A7,A15,A38,A32,A36,A54,Th53 .= (h.m)*(f/.x0); A62: integral(f-g,x0,x0+h.m) = integral(f,x0,x0+h.m) - integral(g,x0,x0+h.m) by A1,A2,A3,A4,A7,A15,A38,A32,A36,A59,A55,Th51; 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) + Z0 -(h.m)*(f/.x0) by RLVECT_1:15 .= integral(f,x0,x0+h.m) - integral(g,x0,x0+h.m) by A61,RLVECT_1:def 4; then R/.(h.m) =integral(f-g,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*e)*abs(h.m)/abs(h.m) by A60,A58,Lm17,XREAL_1:72; then ||.(h.m)"*(R/.(h.m)).|| <= n*e 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 thesis by RLVECT_1:13; end; hence (h")(#)(R/*h) is convergent by NORMSP_1:def 6; hence thesis by A17,NORMSP_1:def 7; end; consider N be Neighbourhood of x0 such that A64: N c= ].a,b.[ by A7,RCOMP_1:18; reconsider R as RestFunc of REAL-NS n by A14,A16,NDIFF_3:def 1; A65: for x be Real st x in N holds F/.x-F/.x0 = L.(x-x0) + R/.(x-x0) proof let x be Real; assume x in N; 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) = F1(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 thesis; 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; reconsider N1=1 as Real; L.1=N1*(f/.x0) by A9 .= f/.x0 by RLVECT_1:def 8; hence thesis by A66,A65,A67,NDIFF_3:def 4; end; Lm18: for f be PartFunc of REAL,REAL-NS n ex F be PartFunc of REAL,REAL-NS n st ].a,b.[ c= dom F & for x be real number st x in ].a,b.[ holds F.x = integral(f,a,x) proof deffunc G(real number) = 0.(REAL-NS n); let f be PartFunc of REAL,REAL-NS n; defpred C[set] means $1 in ].a,b.[; deffunc F(real number) = integral(f,a,$1); consider F be Function such that A1: dom F = REAL & for x be Element of REAL holds (C[x] implies F.x = F(x)) & (not C[x] implies F.x = G(x)) from PARTFUN1:sch 4; now let y be set; assume y in rng F; then consider x be set such that A2: x in dom F and A3: y = F.x by FUNCT_1:def 3; reconsider x as Element of REAL by A1,A2; A4: now assume not x in ].a,b.[; then F.x = 0.(REAL-NS n) by A1; hence y in the carrier of (REAL-NS n) by A3; end; now assume x in ].a,b.[; then F.x = integral(f,a,x) by A1; hence y in the carrier of (REAL-NS n) by A3; end; hence y in the carrier of (REAL-NS n) by A4; end; then rng F c= the carrier of (REAL-NS n) by TARSKI:def 3; then reconsider F as PartFunc of REAL,REAL-NS n by A1,RELSET_1:4; take F; thus thesis by A1; end; theorem for n be non empty Element of NAT, f be 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 & x0 in ].a,b.[ & f is_continuous_in x0 ex F be PartFunc of REAL,REAL-NS n st ].a,b.[ c= dom F & (for x be real number st x in ].a,b.[ holds F.x = integral(f,a,x)) & F is_differentiable_in x0 & diff(F,x0)=f/.x0 proof let n be non empty Element of NAT; let f be PartFunc of REAL,REAL-NS n; consider F be PartFunc of REAL,REAL-NS n such that A1: ].a,b.[ c= dom F & for x be real number st x in ].a,b.[ holds F.x = integral(f,a,x) by Lm18; assume a <= b & f is_integrable_on ['a,b'] & f| ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0; then F is_differentiable_in x0 & diff(F,x0)=f/.x0 by A1,Th55; hence thesis by A1; end;