0; then x-x0 < 0 by A48,XREAL_1:47; then A50: |.x-x0.| = -(x-x0) by ABSVALUE:def 1; |.h.m.| = -(h.m) by A47,XREAL_1:31,ABSVALUE:def 1; hence thesis by A49,A50,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 A30,XXREAL_0:2; 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 .|| <= e by A4,A21,A53; then ||. f/.x- g/.xx .|| <= e by FUNCOP_1:7; hence thesis by A15,A37,A53,VFUNCT_1:def 2; end; B54: now let x be Real; assume B1:x in ['a,b']; thus g/.x = g.x by A36,XREAL_0:def 1,PARTFUN1:def 6 .= f/.x0 by B1,FUNCOP_1:7; end; XX: m in NAT by ORDINAL1:def 12; 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-g,x0,x0+h.m) .|| <= e*|.x0+h.m-x0.| by A1,A7,X1,X2,A37,A41,INTEGR21:25; A61: integral(g,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-g,x0,x0+h.m) = integral(f,x0,x0+h.m) - integral(g,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) + Z0 -(h.m)*(f/.x0) by RLVECT_1:15 .= integral(f,x0,x0+h.m) - integral(g,x0,x0+h.m) by A61; 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)).|| /|.h.m.| & ||.(R/.(h.m)).|| /|.h.m.| <= e*|.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 thesis by A22,A57,XXREAL_0:2; end; hence (h")(#)(R/*h) is convergent; 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 X 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+In(x-x0,REAL) = x0 + (x-x0) & R.(x-x0) = F1(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 thesis; end; A66:N c= dom F by A5,A64; hence A67: F is_differentiable_in x0 by A65; reconsider N1=1 as Real; L/.1 = N1*(f/.x0) by C9; then L/.1 = f/.x0 by RLVECT_1:def 8; hence thesis by A66,A65,A67,NDIFF_3:def 4; end; suppose a > b; hence thesis by A7,XXREAL_1:28; end; end; theorem Th35: for F be PartFunc of REAL,the carrier of X, f be continuous PartFunc of REAL,the carrier of X st dom f =[.a,b.] & dom F =[.a,b.] & for t be Real st t in [.a,b.] holds F/.t = integral(f,a,t) holds for x be Real st x in [.a,b.] holds F is_continuous_in x proof let F be PartFunc of REAL,the carrier of X; let f be continuous PartFunc of REAL,the carrier of X; set f1 = ||.f.||; assume A1: dom f =[.a,b.] & dom F =[.a,b.] & for t be Real st t in [.a,b.] holds F/.t = integral(f,a,t); let x0 be Real; assume A12: x0 in [.a,b.]; per cases; suppose a > b; hence thesis by A12,XXREAL_1:29; end; suppose X1: a<=b; reconsider AB = ['a,b'] as non empty closed_interval Subset of REAL; X2:AB = [.a,b.] by X1,INTEGRA5:def 3; then A2:f|AB is bounded by A1,X1,INTEGR21:11; B1:dom f = dom f1 by NORMSP_0:def 2; then f1|AB = f1 by A1,X2; then f1 is bounded by A1,A2,X2,INTEGR21:9; then consider K be Real such that A3: for y be set st y in dom f1 holds |. f1.y .| < K by COMSEQ_2:def 3; B2:[.a,b.] = AB by X1,INTEGRA5:def 3; then a in AB by X1; then |. f1.a .| < K by A1,X2,B1,A3; then A5:0 < K by COMPLEX1:46; A6:now let c,d be Real; assume A11: c in ['a,b'] & d in ['a,b']; then A7: ['min(c,d),max(c,d)'] c= ['a,b'] by X1,INTEGR19:3; now let y be Real; assume y in ['min(c,d),max(c,d)']; then y in ['a,b'] by A7; then A9: y in dom f1 by X2,NORMSP_0:def 2,A1; then |. f1.y .|< K by A3; then |. ||.f/.y .|| .| < K by A9,NORMSP_0:def 2; hence ||. f/.y .|| <= K by ABSVALUE:def 1; end; hence ||. integral(f,c,d) .|| <= K * |.d-c.| by A1,X1,X2,A11,INTEGR21:25; end; for r be Real st 0y0; set F = F0|[.a,b.], G = G0|[.a,b.]; dom F = dom F0 /\ [.a,b.] & dom G = dom G0 /\ [.a,b.] by RELAT_1:61; then dom F = REAL /\ [.a,b.] & dom G = REAL /\ [.a,b.] by FUNCT_2:def 1; then A6:dom F = [.a,b.] & dom G = [.a,b.] & dom g = dom F /\ dom G by A3,XBOOLE_1:28; A10:].a,b.[ c= [.a,b.] by XXREAL_1:25; A7:for x be Real st x in [.a,b.] holds F/.x = integral(f,a,x) proof let x be Real; assume x in [.a,b.]; then A8: F/.x = F.x & F.x = F0.x by A6,PARTFUN1:def 6,FUNCT_1:47; x in REAL by XREAL_0:def 1; hence F/.x = integral(f,a,x) by A5,A8; end; then A12:for x be Real st x in ].a,b.[ holds F/.x = integral(f,a,x) by A10; A14:now let x be Real; assume A15: x in Z; then f is_continuous_in x by A10,A2,D1,NFCONT_3:def 2; hence F is_differentiable_in x & diff(F,x)=f/.x by A15,A2,D1,A12,A10,A6,Th1955; end; then for x be Real st x in Z holds F is_differentiable_in x; then A16:F is_differentiable_on Z by D1,A6,XXREAL_1:25,NDIFF_3:10; A18:now let x be Real; assume A19: x in [.a,b.]; then G/.x = G.x by A6,PARTFUN1:def 6; then G/.x = G0.x by A19,A6,FUNCT_1:47; hence G/.x = y0 by XREAL_0:def 1,FUNCOP_1:7; end; G|Z is constant; then A23: G is_differentiable_on Z & for x be Real st x in Z holds (G`|Z).x = 0.X by A6,D1,A10,NDIFF_3:20; now let x be Element of REAL; assume A25: x in dom g; then G/.x = y0 & F/.x = integral(f,a,x) by A3,A7,A18; hence g/.x = G/.x + F/.x by A3,D2,A25; end; then A29: g = G + F by A6,VFUNCT_1:def 1; F is continuous by A6,A7,Th35,A2; hence g is continuous by A29; thus B1: g is_differentiable_on Z by A29,A16,A23,A3,D1,A10,NDIFF_3:17; thus for t be Real st t in Z holds diff(g,t) = f/.t proof let t be Real; assume A33: t in Z; then diff(g,t) = (g`|Z).t & (g`|Z).t = diff(G,t) + diff(F,t) & diff(G,t) = (G`|Z).t & (G`|Z).t = 0.X by A23,B1,A29,A16,NDIFF_3:17,def 6; hence diff(g,t) = f/.t by A14,A33; end; end; theorem Th45a: for f be PartFunc of REAL,the carrier of X st a <= b & [.a,b.] c= dom f & (for x be Real st x in [.a,b.] holds f is_continuous_in x) & f is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X holds f/.b = f/.a proof let f be PartFunc of REAL,the carrier of X; assume that A1: a <= b & [.a,b.] c= dom f & for x be Real st x in [.a,b.] holds f is_continuous_in x and A2: f is_differentiable_on ].a,b.[ and A3: for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X; A5:for x be Real st x in ].a,b.[ holds f is_differentiable_in x by A2,NDIFF_3:10; now let x be Real; assume x in ].a,b.[; then ||.diff(f,x).|| = ||. 0.X .|| by A3; hence ||.diff(f,x).|| <= 0; end; then ||. f/.b - f/.a .|| <= 0*|.b-a.| by A5,Th519,A1; then ||. f/.b - f/.a .|| = 0; hence f/.b = f/.a by NORMSP_1:6; end; theorem Th45: for f be PartFunc of REAL,the carrier of X st [.a,b.] c= dom f & (for x be Real st x in [.a,b.] holds f is_continuous_in x) & f is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X holds f|(].a,b.[) is constant proof let f be PartFunc of REAL,the carrier of X; assume that A1: [.a,b.] c= dom f & for x be Real st x in [.a,b.] holds f is_continuous_in x and A2: f is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X; now let x1,x2 be Element of REAL; assume x1 in ].a,b.[ /\ dom f & x2 in ].a,b.[ /\ dom f; then A4: x1 in ].a,b.[ & x2 in ].a,b.[ by XBOOLE_0:def 4; reconsider Z1=].x1,x2.[, Z2=].x2,x1.[ as open Subset of REAL; A7: ].a,b.[ c= [.a,b.] & Z1 c= [.x1,x2.] & Z2 c= [.x2,x1.] by XXREAL_1:25; then [.x1,x2.] c= [.a,b.] & [.x2,x1.] c= [.a,b.] by A4,XXREAL_2:def 12; then C1: [.x1,x2.] c= dom f & [.x2,x1.] c= dom f & (for x be Real st x in [.x1,x2.] holds f is_continuous_in x) & (for x be Real st x in [.x2,x1.] holds f is_continuous_in x) by A1; [.x1,x2.] c= ].a,b.[ & [.x2,x1.] c= ].a,b.[ by A4,XXREAL_2:def 12; then (f is_differentiable_on Z1 & for x be Real st x in Z1 holds diff(f,x) = 0.X) & (f is_differentiable_on Z2 & for x be Real st x in Z2 holds diff(f,x) = 0.X) by A2,A7,NDIFF_3:24,XBOOLE_1:1; then (x1 < x2 implies f/.x1 = f/.x2) & (x2 < x1 implies f/.x1 = f/.x2) by C1,Th45a; hence f/.x1 = f/.x2 by XXREAL_0:1; end; hence f| (].a,b.[) is constant by PARTFUN2:36; end; theorem Th46: for f be continuous PartFunc of REAL,the carrier of X st [.a,b.] = dom f & f | ].a,b.[ is constant holds for x be Real st x in [.a,b.] holds f/.x = f/.a proof let f be continuous PartFunc of REAL,the carrier of X; assume A1: [.a,b.] = dom f & f| (].a,b.[) is constant; A2:].a,b.[ c= [.a,b.] by XXREAL_1:25; per cases; suppose X0: a >= b; hereby let x be Real; assume x in [.a,b.]; then a <= x & x <= b by XXREAL_1:1; then a <= x & x <= a by X0,XXREAL_0:2; hence f/.x = f/.a by XXREAL_0:1; end; end; suppose A0: a < b; reconsider d = (b-a)/2 as Real; A3: 0 < b-a by A0,XREAL_1:50; then A4: 0 < d by XREAL_1:215; a+(b-a)/2 = (a+b) / 2; then A5: a < a+d & a+d < b by A0,XREAL_1:226; then a+d in ].a,b.[; then f.(a+d) in rng f by A2,A1,FUNCT_1:3; then reconsider f0=f.(a+d) as Point of X; dom (f| (].a,b.[) ) = dom f /\ (].a,b.[) by RELAT_1:61; then A6: dom (f| (].a,b.[) ) = ].a,b.[ by A1,XXREAL_1:25,XBOOLE_1:28; A7: now let x be Real; assume A8: x in ].a,b.[; A9: a+d in dom (f| (].a,b.[) ) by A5,A6; thus f/.x = f.x by A8,A2,A1,PARTFUN1:def 6 .= (f| (].a,b.[) ).x by A6,A8,FUNCT_1:47 .= (f| (].a,b.[) ).(a+d) by A1,A6,A8,A9,FUNCT_1:def 10 .=f0 by A9,FUNCT_1:47; end; a in dom f & b in dom f by A1,A0; then A14:f is_continuous_in a & f is_continuous_in b by NFCONT_3:def 2; deffunc F1(Nat) = a+d/($1+1); A12:for x being Element of NAT holds F1(x) is Element of REAL by XREAL_0:def 1; consider s1 be Real_Sequence such that A13: for x being Element of NAT holds s1.x = F1(x) from FUNCT_2:sch 9(A12); A15:now let y be object; assume y in rng s1; then consider x be object such that A16: x in dom s1 & y=s1.x by FUNCT_1:def 3; reconsider x as Element of NAT by A16; A17: y = a+d/(x+1) by A13,A16; 0 < d/(x+1) by A4,XREAL_1:139; then A20: a + (0 qua Real) < a + d/(x+1) by XREAL_1:8; 1 + (0 qua Real) <= 1 + x by XREAL_1:7; then d/(x+1) <= d / 1 by XREAL_1:118,A3; then a + d/(x+1) <= a + d by XREAL_1:7; then a + d/(x+1) < b by A5,XXREAL_0:2; hence y in ].a,b.[ by A17,A20; end; then A21:rng s1 c= ].a,b.[ & rng s1 c= dom f by A2,A1; A23:now let p be Real; assume A24: 0 Function of R_NormSpace_of_ContinuousFunctions(['a,b'],X), R_NormSpace_of_ContinuousFunctions(['a,b'],X) means :Def8: for x be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X) ex f,g,Gf be continuous PartFunc of REAL,the carrier of X st x=f & it.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f & for t be Real st t in ['a,b'] holds g/.t = y0 + integral(Gf,a,t); existence proof defpred P[set,set] means ex f,g,Gf be continuous PartFunc of REAL,the carrier of X st $1=f & $2=g & dom f =['a,b'] & dom g =['a,b'] & Gf=G*f & for t be Real st t in ['a,b'] holds g/.t = y0+ integral(Gf,a,t); set D = the carrier of R_NormSpace_of_ContinuousFunctions(['a,b'],X); X1:the carrier of X = dom G by FUNCT_2:def 1; A2:for x being Element of D ex y being Element of D st P[x,y] proof let x be Element of D; consider f0 be continuous PartFunc of REAL,the carrier of X such that A3: x=f0 & dom f0 = ['a,b'] by ORDEQ_01:def 2; now let x0 be Real; assume A4: x0 in dom(G*f0); then f0 is_continuous_in x0 by NFCONT_3:def 2,FUNCT_1:11; hence G*f0 is_continuous_in x0 by A4,X1,NFCONT_3:15,A1; end; then reconsider Gf = G*f0 as continuous PartFunc of REAL,the carrier of X by NFCONT_3:def 2; rng f0 c= dom G by X1; then A6: dom Gf = ['a,b'] by A3,RELAT_1:27; A7: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; deffunc FX(Element of REAL) = integral(Gf,a,$1); consider F0 be Function of REAL,the carrier of X such that A8: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4; set F = F0|['a,b']; dom F0 = REAL by FUNCT_2:def 1; then A9: dom F = ['a,b'] by RELAT_1:62; A10:now let t be Real; assume A11: t in [.a,b.]; A12: t in REAL by XREAL_0:def 1; thus F/.t = F.t by A7,A9,A11,PARTFUN1:def 6 .= F0.t by A11,A9,A7,FUNCT_1:47 .= integral(Gf,a,t) by A8,A12; end; set G0 = REAL --> y0; set G1 = G0| ['a,b']; dom G0 = REAL by FUNCT_2:def 1; then A14:dom G1 = ['a,b'] by RELAT_1:62; A15:now let t be Real; assume A16: t in [.a,b.]; hence G1/.t = G1.t by A7,A14,PARTFUN1:def 6 .= G0.t by A16,A14,A7,FUNCT_1:47 .= y0 by XREAL_0:def 1,FUNCOP_1:7; end; set g=G1+F; A19:dom g = dom F /\ dom G1 by VFUNCT_1:def 1 .= ['a,b'] by A9,A14; F is continuous by A7,A9,Th35,A6,A10; then reconsider g as continuous PartFunc of REAL,the carrier of X; reconsider y=g as Element of D by A19,ORDEQ_01:def 2; take y; now let t be Real; assume A20:t in ['a,b']; then G1/.t = y0 & F/.t = integral(Gf,a,t) by A7,A10,A15; hence g/.t = y0 + integral(Gf,a,t) by A19,A20,VFUNCT_1:def 1; end; hence thesis by A19,A3; end; consider F being Function of D,D such that A23:for x being Element of D holds P[x,F.x] from FUNCT_2:sch 3 (A2); take F; thus thesis by A23; end; uniqueness proof let F1,F2 be Function of R_NormSpace_of_ContinuousFunctions(['a,b'],X), R_NormSpace_of_ContinuousFunctions(['a,b'],X); assume A24:for x be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X) holds ex f,g,Gf be continuous PartFunc of REAL,the carrier of X st x=f & F1.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f & for t be Real st t in ['a,b'] holds g/.t = y0+ integral(Gf,a,t); assume A25:for x be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X) holds ex f,g,Gf be continuous PartFunc of REAL,the carrier of X st x=f & F2.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f & for t be Real st t in ['a,b'] holds g/.t = y0+ integral(Gf,a,t); now let x be Element of R_NormSpace_of_ContinuousFunctions(['a,b'],X); consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X such that A26: x=f1 & F1.x = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1 & for t be Real st t in ['a,b'] holds g1/.t = y0+ integral(Gf1,a,t) by A24; consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X such that A27: x=f2 & F2.x = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2 & for t be Real st t in ['a,b'] holds g2/.t = y0+ integral(Gf2,a,t) by A25; now let t be object; assume A28: t in dom g1; then reconsider t0=t as Real; A29: g1/.t = y0+ integral(Gf2,a,t0) by A27,A28,A26 .= g2/.t by A28,A27,A26; thus g1.t = g1/.t by A28,PARTFUN1:def 6 .= g2.t by A26,A27,A28,A29,PARTFUN1:def 6; end; hence F1.x = F2.x by A26,A27,FUNCT_1:2; end; hence F1=F2 by FUNCT_2:def 8; end; end; theorem Th53: a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) implies for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X), g,h be continuous PartFunc of REAL,the carrier of X st g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v holds for t be Real st t in ['a,b'] holds ||. g/.t - h/.t .|| <= r*(t-a)*||.u-v.|| proof assume A1: a<=b & 0 < r & for y1, y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; A2:dom G = the carrier of X by FUNCT_2:def 1; for x1,x2 be Point of X st x1 in (the carrier of X) & x2 in (the carrier of X) holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then G is_Lipschitzian_on the carrier of X by A1,FUNCT_2:def 1; then A3:G is_continuous_on dom G by A2,NFCONT_1:45; let u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X), g,h be continuous PartFunc of REAL,the carrier of X; assume A4: g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v; set F= Fredholm(G,a,b,y0); consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X such that A5: u=f1 & F.u = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1 & for t be Real st t in ['a,b'] holds g1/.t = y0+ integral(Gf1,a,t) by Def8,A1,A3; consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X such that A6: v=f2 & F.v = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2 & for t be Real st t in ['a,b'] holds g2/.t = y0+ integral(Gf2,a,t) by Def8,A1,A3; set Gf12= Gf1 - Gf2; dom G = the carrier of X by FUNCT_2:def 1; then rng f1 c= dom G & rng f2 c= dom G; then A8:dom Gf1 =['a,b'] & dom Gf2 =['a,b'] by A5,A6,RELAT_1:27; reconsider Gf12 as continuous PartFunc of REAL,the carrier of X; A10:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then A18:a in ['a,b'] by A1; let t be Real; assume A11: t in ['a,b']; then A12:ex g be Real st t=g & a<=g & g <= b by A10; then A20:['a,t'] c= ['a,b'] by INTEGR19:1; X1:['a,t'] = [.a,t.] by A12,INTEGRA5:def 3; A13:dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2; for x be Real st x in ['a,t'] holds ||. Gf12/.x .|| <= r*||.u-v.|| proof let x be Real; assume A19: x in ['a,t']; then A21:Gf12/.x =Gf1/.x -Gf2/.x by A8,A13,A20,VFUNCT_1:def 2; A24:r*||.(f1/.x)-(f2/.x).|| <=r*||.u-v.|| by A1,XREAL_1:64,A19,A20,A5,A6,ORDEQ_01:26; A22:Gf1/.x = (Gf1).x by A8,A20,A19,PARTFUN1:def 6 .= G.(f1.x) by A20,A19,A8,A5,FUNCT_1:12 .= G/.(f1/.x) by A20,A19,A5,PARTFUN1:def 6; Gf2/.x = (Gf2).x by A8,A20,A19,PARTFUN1:def 6 .= G.(f2.x) by A20,A19,A8,A6,FUNCT_1:12 .= G/.(f2/.x) by A20,A19,A6,PARTFUN1:def 6; then ||. Gf1/.x -Gf2/.x .||<=r*||.(f1/.x)-(f2/.x).|| by A22,A1; hence thesis by A21,A24,XXREAL_0:2; end; then A25: ||. integral(Gf12,a,t) .||<= r*||.u-v.||*(t-a) by Lm14a,X1,A8,A13,A18,A10,A11,A12; g/.t = y0 + integral(Gf1,a,t) & h/.t = y0 + integral(Gf2,a,t) by A4,A5,A6,A11; then g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by RLVECT_1:27 .= integral(Gf1,a,t) + (y0 - y0) -integral(Gf2,a,t) by RLVECT_1:28 .= integral(Gf1,a,t) + 0.X -integral(Gf2,a,t) by RLVECT_1:15 .= integral(Gf12,a,t) by A8,A18,A11,A1,INTEGR21:30; hence thesis by A25; end; theorem Th54: a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) implies for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X), m be Element of NAT, g,h be continuous PartFunc of REAL,the carrier of X st g = iter(Fredholm(G,a,b,y0),(m+1)).u & h = iter(Fredholm(G,a,b,y0),(m+1)).v holds for t be Real st t in ['a,b'] holds ||. g/.t - h/.t .|| <= ((r*(t-a))|^(m+1))/((m+1)!) * ||.u-v.|| proof assume A1: a<=b & 0 < r & for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; set F = Fredholm(G,a,b,y0); A2:dom G = the carrier of X by FUNCT_2:def 1; for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then G is_Lipschitzian_on the carrier of X by A1,FUNCT_2:def 1; then A3:G is_continuous_on dom G by A2,NFCONT_1:45; let u1,v1 be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X); defpred P[Nat] means for g,h be continuous PartFunc of REAL,the carrier of X st g = iter(F,($1+1)).u1 & h = iter(F,($1+1)).v1 holds for t be Real st t in ['a,b'] holds ||. g/.t - h/.t .|| <= ((r*(t-a))|^($1+1))/(($1+1)!) * ||.u1-v1.||; reconsider Z0 = 0 as Element of NAT; A4:P[0] proof let g,h be continuous PartFunc of REAL,the carrier of X; assume g = iter(F,( (0 qua Element of NAT ) + 1)).u1 & h = iter(F,( (0 qua Element of NAT ) + 1)).v1; then A6: g= F.u1 & h= F.v1 by FUNCT_7:70; now let t be Real; assume t in ['a,b']; then ||. g/.t - h/.t .|| <= r*(t-a) * ||.u1-v1.|| by Th53,A1,A6; hence ||. g/.t - h/.t .|| <= ((r*(t-a))|^(Z0 + 1) ) /((Z0 + 1)!) * ||.u1-v1.|| by NEWTON:13; end; hence thesis; end; A8:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A9: P[k]; let g,h be continuous PartFunc of REAL,the carrier of X; assume A10: g = iter(F,((k+1)+1)).u1 & h = iter(F,((k+1)+1)).v1; reconsider u=iter(F,(k+1)).u1, v=iter(F,(k+1)).v1 as VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X); A11:dom iter(F,k+1) = the carrier of R_NormSpace_of_ContinuousFunctions(['a,b'],X) by FUNCT_2:def 1; A12:iter(F,((k+1)+1)).u1 = (F*iter(F,k+1)).u1 by FUNCT_7:71 .= F.u by A11,FUNCT_1:13; A13:iter(F,((k+1)+1)).v1 = (F*iter(F,k+1)).v1 by FUNCT_7:71 .= F.v by A11,FUNCT_1:13; consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X such that A14: u=f1 & F.u = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1 & for t be Real st t in ['a,b'] holds g1/.t = y0+ integral(Gf1,a,t) by Def8,A1,A3; consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X such that A15: v=f2 & F.v = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2 & for t be Real st t in ['a,b'] holds g2/.t = y0+ integral(Gf2,a,t) by Def8,A1,A3; set Gf12= Gf1 - Gf2; dom G = the carrier of X by FUNCT_2:def 1; then rng f1 c= dom G & rng f2 c= dom G; then A18:dom Gf1 =['a,b'] & dom Gf2 =['a,b'] by A14,A15,RELAT_1:27; reconsider Gf12 as continuous PartFunc of REAL,the carrier of X; A20:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; let t be Real; assume A21: t in ['a,b']; then A22:ex g be Real st t=g & a<=g & g <= b by A20; a22:ex g be Element of REAL st t=g & a<=g & g <= b proof consider g be Real such that H1: t=g & a<=g & g <= b by A21,A20; reconsider g as Element of REAL by XREAL_0:def 1; take g; thus thesis by H1; end; A23:dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2 .= ['a,b'] by A18; then A24:dom ||.Gf12.|| = ['a,b'] by NORMSP_0:def 2; A27:a in ['a,b'] by A20,A1; min(a,t) = a & max(a,t) = t by A22,XXREAL_0:def 9,def 10; then A30:||.Gf12.|| is_integrable_on ['a,t'] & (||.Gf12.||) | ['a,t'] is bounded & ||.integral(Gf12,a,t).|| <= integral(||.Gf12.||,a,t) by A1,A23,A27,A21,INTEGR21:22; ['a,t'] = [.a,t.] by A22,INTEGRA5:def 3; then consider rg be PartFunc of REAL,REAL such that A31: dom rg = ['a,t'] & (for x be Real st x in ['a,t'] holds rg.x = r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.|| )) & rg is continuous & rg is_integrable_on ['a,t'] & rg| ['a,t'] is bounded & integral(rg,a,t) = ((r*(t-a))|^((k+1)+1)) / (((k+1)+1)!) * ||.u1-v1.|| by Lm7,a22; A32:['a,t'] c= ['a,b'] by A22,INTEGR19:1; for x be Real st x in ['a,t'] holds ||.Gf12.||.x <= rg.x proof let x be Real; assume A33: x in ['a,t']; then A34: Gf12/.x =Gf1/.x -Gf2/.x by A23,A32,VFUNCT_1:def 2; A35: Gf1/.x = (Gf1).x by A18,A32,A33,PARTFUN1:def 6 .= G.(f1.x) by A32,A33,A18,A14,FUNCT_1:12 .= G/.(f1/.x) by A32,A33,A14,PARTFUN1:def 6; Gf2/.x = (Gf2).x by A18,A32,A33,PARTFUN1:def 6 .= G.(f2.x) by A32,A33,A18,A15,FUNCT_1:12 .= G/.(f2/.x) by A32,A33,A15,PARTFUN1:def 6; then A37: ||. Gf1/.x -Gf2/.x .|| <= r*||.(f1/.x)-(f2/.x).|| by A35,A1; r*||.(f1/.x)-(f2/.x).|| <=r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.||) by A1,XREAL_1:64,A9,A14,A15,A32,A33; then r*||.(f1/.x)-(f2/.x).|| <=rg.x by A33,A31; then ||. Gf1/.x -Gf2/.x .|| <=rg.x by A37,XXREAL_0:2; hence thesis by A24,A32,A33,NORMSP_0:def 2,A34; end; then A38:integral(||.Gf12.||,a,t) <= integral(rg,a,t) by A30,A22,A24,A32,A31,ORDEQ_01:48; g/.t = y0+ integral(Gf1,a,t) & h/.t = y0+ integral(Gf2,a,t) by A14,A15,A21,A12,A10,A13; then g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by RLVECT_1:27 .= integral(Gf1,a,t) + (y0 - y0) -integral(Gf2,a,t) by RLVECT_1:28 .= integral(Gf1,a,t) + 0.X -integral(Gf2,a,t) by RLVECT_1:15 .= integral(Gf12,a,t) by A18,A27,A21,A1,INTEGR21:30; hence thesis by A38,A30,XXREAL_0:2,A31; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A8); hence thesis; end; Lm8: for r,L,a,b,t be Real,m be Nat st a<=t & t <= b & 0 <= L & 0<=r holds ((r*(t-a))|^(m+1))/((m+1)!) * L <= ((r*(b-a))|^(m+1))/((m+1)!) * L proof let r,L,a,b,t be Real, m be Nat; assume A1: a<=t & t <= b & 0 <= L & 0<=r; then t-a <= b-a by XREAL_1:13; then A2:r*(t-a) <= r*(b-a) by A1,XREAL_1:64; 0 <= t-a by A1,XREAL_1:48; then A3:(r*(t-a)) to_power (m+1) <= (r*(b-a)) to_power (m+1) by A1,HOLDER_1:3,A2; ((r*(t-a))|^(m+1))/((m+1)!) <= ((r*(b-a))|^(m+1))/((m+1)!) by A3,XREAL_1:72; hence thesis by A1,XREAL_1:64; end; Lm9: a < b & 0 < r implies ex m be Element of NAT st ((r*(b-a))|^(m+1))/((m+1)!) < 1 & 0 < ((r*(b-a))|^(m+1))/((m+1)!) proof assume A1: a < b & 0 < r; set z=r*(b-a); set s = z rExpSeq; s is summable by SIN_COS:45; then s is convergent & lim s = 0 by SERIES_1:4; then consider n be Nat such that A3: for m be Nat st n<=m holds |.s.m- 0 .| < 1 by SEQ_2:def 7; reconsider m0 = max(n,1) as Element of NAT by ORDINAL1:def 12; reconsider m = m0 - 1 as Element of NAT by INT_1:5,XXREAL_0:25; take m; |.s.(m+1) - 0 .| < 1 by A3,XXREAL_0:25; then A4:|. ((r*(b-a))|^(m+1))/((m+1)!) .| < 1 by SIN_COS:def 5; 0 < b - a by A1,XREAL_1:50; then (0 qua Real) *r < r*(b-a) by A1,XREAL_1:68; then 0 < (r*(b-a)) to_power (m+1) by POWER:34; hence thesis by A4,ABSVALUE:def 1,XREAL_1:139; end; theorem Th55: for m be Nat st a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) holds for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X) holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u - iter(Fredholm(G,a,b,y0),(m+1)).v .|| <= ((r*(b-a))|^(m+1))/((m+1)!) * ||.u-v.|| proof let m be Nat; assume A1: a<=b & 0 < r & for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; let u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X); reconsider u1=iter(Fredholm(G,a,b,y0),(m+1)).u as VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X); reconsider v1=iter(Fredholm(G,a,b,y0),(m+1)).v as VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X); consider g be continuous PartFunc of REAL,the carrier of X such that A2: u1=g & dom g = ['a,b'] by ORDEQ_01:def 2; consider h be continuous PartFunc of REAL,the carrier of X such that A3: v1=h & dom h = ['a,b'] by ORDEQ_01:def 2; now let t be Real; A4: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; assume A5: t in ['a,b']; then A6: ex g be Real st t=g & a<=g & g <= b by A4; m in NAT by ORDINAL1:def 12; then A7: ||. g/.t - h/.t .|| <= ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A5,Th54,A1,A2,A3; ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A6,A1,Lm8; hence ||. g/.t - h/.t .|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A7,XXREAL_0:2; end; hence thesis by ORDEQ_01:27,A2,A3; end; theorem Th56: a < b & G is_Lipschitzian_on the carrier of X implies ex m be Nat st iter(Fredholm(G,a,b,y0),(m+1)) is contraction proof assume A1: a