0; x0 + h.m - x0 < x0-x0 by A47,XREAL_1:14; then A51: |.h.m.| = -(h.m) by ABSVALUE:def 1; x-x0 < 0 by A48,A50,XREAL_1:47; then |.x-x0.| = -(x-x0) by ABSVALUE:def 1; hence thesis by A49,A51,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 A52: |.x-x0.| < r by A31,XXREAL_0:2; then x in ].x0-r,x0+r.[ by RCOMP_1:1; then x in ].x0-q,x0+q.[ by A30; then x in ].a,b.[ by A25,A27; then A53: x in [.a,b.] by A38; A54: x1 in REAL by XREAL_0:def 1; |.x-x0.| < p/2 by A40,A52,XXREAL_0:2; then |.x-x0.| < p by A24,XXREAL_0:2; then |.f.x- f.x0.|<=e by A4,A16,A22,A53; then |.f.x1- g.x1.|<=e by FUNCOP_1:7,A54; hence thesis by A16,A37,A53,VALUED_1:13; end; A55: for x be Real st x in [' a,b '] holds g.x = f.x0 by FUNCOP_1:7; then A56: g|[' a,b '] is bounded by A1,A36,Th26; then A57: (f-g)|(['a,b '] /\ ['a,b ']) is bounded by A3,RFUNCT_1:84; A58: m in NAT by ORDINAL1:def 12; rng h c= dom R by A11; then R.(h.m)/(h.m) =(R/*h).m /(h.m) by FUNCT_2:108,A58; then R.(h.m)/(h.m) =((R/*h).m) *((h").m) by VALUED_1:10; then A59: R.(h.m)/(h.m) = ((h")(#)(R/*h)).m by SEQ_1:8; h.m <> 0 by SEQ_1:4,A58; then A60: 0 < |.h.m.| by COMPLEX1:47; A61: g is_integrable_on [' a,b '] by A1,A36,A55,Th26; then f-g is_integrable_on [' a,b '] by A2,A3,A4,A36,A56,Th11; then A62: |.integral(f-g,x0,x0+h.m).| <= e*|.x0+h.m-x0.| by A1,A7,A16,A38,A33,A57 ,A37,A41,Lm8; integral(g,x0,x0+h.m)=(f.x0)*((x0+h.m)-x0) by A1,A7,A16,A38,A33,A36,A55 ,Th27; then R.(h.m) =integral(f-g,x0,x0+h.m) by A1,A2,A3,A4,A7,A16,A38,A33,A35 ,A36,A61,A56,A39,Th24; then |.R.(h.m)/(h.m).| = |.R.(h.m).|/|.h.m.| & |.R.(h.m).|/|.h.m.| <= e*|. h.m.|/|.h.m.| by A62,A60,COMPLEX1:67,XREAL_1:72; then A63: |.R.(h.m)/(h.m).| <= e by A60,XCMPLX_1:89; e < e0 by A20,XREAL_1:216; hence thesis by A63,A59,XXREAL_0:2; end; hence (h")(#)(R/*h) is convergent by SEQ_2:def 6; hence thesis by A18,SEQ_2: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 by A15,A17,FDIFF_1:def 2; 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 A66:x0 + (x-x0) in N; reconsider x as Real; A67: x0+(x-x0) in N by A66; C1[x-x0] by A67,A64; then R.(x-x0) = F1(x-x0) by A11; hence thesis; end; A68: N c= dom F by A5,A64; hence A69: F is_differentiable_in x0 by A65,FDIFF_1:def 4; L.1=(f.x0)*1 by A10; hence thesis by A68,A65,A69,FDIFF_1:def 5; end; Lm13: for a,b be Real, f be PartFunc of REAL,REAL holds ex F be PartFunc of REAL,REAL 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; let a,b be Real; let f be PartFunc of REAL,REAL; 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 = In(0,REAL) by A1; hence y in REAL by A3; end; now assume x in ].a,b.[; then F.x = integral(f,a,x) by A1; hence y in REAL by A3,XREAL_0:def 1; end; hence y in REAL by A4; end; then rng F c= REAL; then reconsider F as PartFunc of REAL,REAL by A1,RELSET_1:4; take F; thus thesis by A1; end; theorem for x0 be Real 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 holds ex F be PartFunc of REAL,REAL 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 x0 be Real; consider F be PartFunc of REAL,REAL 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 Lm13; 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,Th28; hence thesis by A1; end;