0; 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 thesis by A51,A53,XREAL_1:24; end; suppose x-x0 = 0; then |.x-x0.| = 0 by ABSVALUE:def 1; hence thesis by COMPLEX1:46; end; end; end; then A54: |.x-x0.| < r by A32,XXREAL_0:2; then x in ].x0-r,x0+r.[ 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 .|| <= e by A4,A17,A23,A55; then ||. f/.x- g/.xx .|| <= e by FUNCOP_1:7; hence thesis by A17,A39,A55,VFUNCT_1:def 2; end; A56: for x be Real st x in ['a,b'] holds g.x = f/.x0 by FUNCOP_1:7; then A57: g| ['a,b'] is bounded by A1,A38,Th51; then A58: (f-g) | (['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: g is_integrable_on ['a,b'] by A1,A38,A56,Th51; then A63: ||. integral(f-g,x0,x0+h.m) .|| <= (n*e)*|.x0+h.m-x0.| by A1,A7,A17,A40,A34,A58,A39,A43,Th54,A2,A4,A38,INTEGR18:15; A64: integral(g,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-g,x0,x0+h.m) = integral(f,x0,x0+h.m) - integral(g,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) + Z0 -(h.m)*(f/.x0) by RLVECT_1:15 .= integral(f,x0,x0+h.m) - integral(g,x0,x0+h.m) by A64,RLVECT_1:def 4; then R/.(h.m) =integral(f-g,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*e)*|.h.m.|/|.h.m.| by A63,A61,Lm17,XREAL_1:72; then ||.(h.m)"*(R/.(h.m)).|| <= n*e 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 thesis by RLVECT_1:13; end; hence (h")(#)(R/*h) is convergent by NORMSP_1:def 6; hence thesis by A19,NORMSP_1:def 7; end; consider N be Neighbourhood of x0 such that A67: N c= ].a,b.[ by A7,RCOMP_1:18; reconsider R as RestFunc of REAL-NS n by A16,A18,NDIFF_3:def 1; A68: 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 A69: x0+In(x-x0,REAL) in N; then A70: x0+In(x-x0,REAL) = x0 + (x-x0) & R.(x-x0) = F1(x-x0) by A12,A67; x0+In(x-x0,REAL) in ].a,b.[ by A69,A67; then A71: C1[x-x0]; R/.(x-x0) = R.(x-x0) by A12,PARTFUN1:def 6,A70 .= F1(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 thesis; end; A72: N c= dom F by A5,A67; hence A73: F is_differentiable_in x0 by A68,NDIFF_3:def 3; reconsider N1=1 as Real; L/.1=N1*(f/.x0) by A11 .= f/.x0 by RLVECT_1:def 8; hence thesis by A72,A68,A73,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 st x in ].a,b.[ holds F.x = integral(f,a,x) proof deffunc G(Real) = 0.(REAL-NS n); let f be PartFunc of REAL,REAL-NS n; defpred C[set] means $1 in ].a,b.[; deffunc F(Real) = 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 object; assume y in rng F; then consider x be object 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); 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 zero 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 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 zero 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 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;