0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds ( |. z .|"* |. R/.z .|) < r; thus R is total by A1; let s be non-zero 0-convergent Real_Sequence; A21: s is convergent & lim s = 0; A22: now let r be Real; assume r > 0; then consider d be Real such that A23: d > 0 and A24: for z be Real st z <> 0 & |. z .| < d holds ( |. z .| "* |. R/.z .|) < r by A20; consider n0 be Nat such that A25: for m be Nat st n0 <=m holds |. s.m-0 .| < d by A21,A23,SEQ_2:def 7; take n0; thus for m be Nat st n0 <=m holds |. ((s")(#)(R/*s)).m- 0 .| < r proof dom R = REAL by A1,PARTFUN1:def 2; then A26: rng s c= dom R; let m be Nat; A27: m in NAT by ORDINAL1:def 12; assume n0 <= m; then A28: |. s.m-0 .| < d by A25; |. s.m .|" * |.(R/.(s.m)).| = |.((s.m)").| * |.(R/.(s.m)).| by COMPLEX1:66 .= |.(s.m)"*(R/.(s.m)).| by COMPLEX1:65 .= |.(s.m)"*((R/*s).m).| by A26,FUNCT_2:109,A27 .= |.(s".m)*((R/*s).m).| by VALUED_1:10 .= |. ((s")(#)(R/*s)).m- 0 .| by SEQ_1:8; hence thesis by A24,A28,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by SEQ_2:def 6; hence lim ((s")(#)(R/*s)) = 0 by A22,SEQ_2:def 7; end; reserve Z for open Subset of REAL, y0 for VECTOR of REAL-NS n, G for Function of REAL-NS n,REAL-NS n; theorem Th36: for f be continuous PartFunc of REAL,REAL-NS n, g be PartFunc of REAL,REAL-NS n st a <= b & dom f = [' a,b '] & dom g = [' a,b '] & Z = ]. a,b .[ & for t be Real st t in [' a,b '] holds g.t = y0+ integral(f,a,t) holds g is continuous & g/.a=y0 & g is_differentiable_on Z & for t be Real st t in Z holds diff(g,t) = f/.t proof let f be continuous PartFunc of REAL,REAL-NS n, g be PartFunc of REAL,REAL-NS n; assume A1:a <= b & dom f = [' a,b '] & dom g = [' a,b '] & Z = ]. a,b .[ & for t be Real st t in [' a,b '] holds g.t = y0+ integral(f,a,t); A2: f is_integrable_on ['a,b'] by A1,Th33; A3: f| ['a,b'] is bounded by A1,Th32; A4: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; deffunc FX(Element of REAL) = integral(f,a,$1); consider F0 be Function of REAL,REAL-NS n such that A5: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4; set F = F0| ['a,b']; A6: dom F = dom F0 /\ ['a,b'] by RELAT_1:61 .= REAL /\ ['a,b'] by FUNCT_2:def 1 .= ['a,b'] by XBOOLE_1:28; A7: now let x be Real; assume x in [.a,b.]; then A8: x in ['a,b'] by A1,INTEGRA5:def 3; A9: x in REAL by XREAL_0:def 1; thus F.x = F0.x by A8,A6,FUNCT_1:47 .= integral(f,a,x) by A5,A9; end; A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25; A11: for x be Real st x in [.a,b.] holds F is_continuous_in x by Th34,A1,A6,A7; A12: for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) by A7,A10; A13: Z c= dom F by A1,A6,A10,INTEGRA5:def 3; A14: now let x be Real; assume A15: x in Z; then f is_continuous_in x by A10,A4,A1,NFCONT_3:def 2; hence F is_differentiable_in x & diff(F,x)=f/.x by A15,A1,A2,A3,A12,A13,INTEGR19:55; end; then for x be Real st x in Z holds F is_differentiable_in x; then A16: F is_differentiable_on Z by A13,NDIFF_3:10; set G0 = REAL --> y0; set G = G0| ['a,b']; A17: dom G = dom G0 /\ ['a,b'] by RELAT_1:61 .= REAL /\ ['a,b'] by FUNCT_2:def 1 .= ['a,b'] by XBOOLE_1:28; A18: now let x be Real; assume x in [.a,b.]; then A19: x in ['a,b'] by A1,INTEGRA5:def 3; thus G.x = G0.x by A19,A17,FUNCT_1:47 .= y0 by XREAL_0:def 1,FUNCOP_1:7; end; A20: F is continuous by A4,A6,A11,NFCONT_3:def 2; A21: G|Z is constant; then A22: G is_differentiable_on Z & for x be Real st x in Z holds (G`|Z).x = 0.(REAL-NS n) by A17,A1,A10,A4,NDIFF_3:20; A23: dom g = dom F /\ dom G by A6,A17,A1; now let x be Element of REAL; assume A24: x in dom g; A25: x in [.a,b.] by A24,A1,INTEGRA5:def 3; A26: G/.x = G.x by A24,A1,A17,PARTFUN1:def 6 .= y0 by A25,A18; A27: F/.x = F.x by A24,A1,A6,PARTFUN1:def 6 .= integral(f,a,x) by A25,A7; thus g/.x = g.x by A24,PARTFUN1:def 6 .= G/.x + F/.x by A26,A27,A1,A24; end; then A28: g = G + F by A23,VFUNCT_1:def 1; thus g is continuous by A20,A28; A29: a in ['a,b'] by A1,A4; A30: 0.(REAL-NS n) =integral(f,a,a) - integral(f,a,a) by RLVECT_1:15 .= integral(f,a,a) + integral(f,a,a) - integral(f,a,a) by A29,A1,Th33,A3,INTEGR19:53 .= integral(f,a,a) + ( integral(f,a,a) - integral(f,a,a) ) by RLVECT_1:28 .= integral(f,a,a) + 0.(REAL-NS n) by RLVECT_1:15 .= integral(f,a,a); thus g/.a = g.a by A1,A29,PARTFUN1:def 6 .= y0+ integral(f,a,a) by A1,A29 .= y0 by A30; A31: g is_differentiable_on Z & for x be Real st x in Z holds (g`|Z).x = diff(G,x) + diff(F,x) by A28,A16,A22,A1,A10,A4,NDIFF_3:17; thus g is_differentiable_on Z by A28,A16,A22,A1,A10,A4,NDIFF_3:17; thus for t be Real st t in Z holds diff(g,t) = f/.t proof let t be Real; assume A32: t in Z; A33: diff(g,t) =(g`|Z).t by A31,A32,NDIFF_3:def 6 .=diff(G,t) + diff(F,t) by A28,A16,A22,A1,A10,A4,NDIFF_3:17,A32; A34: diff(G,t) = (G`|Z).t by A22,A32,NDIFF_3:def 6 .= 0.(REAL-NS n) by A21,A17,A1,A10,A4,NDIFF_3:20,A32; thus diff(g,t) = 0.(REAL-NS n) + f/.t by A33,A34,A14,A32 .= f/.t; end; end; theorem for i be Nat, y1,y2 be Point of REAL-NS n holds proj(i,n).(y1 + y2) = proj(i,n).y1 + proj(i,n).y2 proof let i be Nat, y1,y2 be Point of REAL-NS n; reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def 4; reconsider ry1 = yy1.i as Real; reconsider ry2 = yy2.i as Real; A1: proj(i,n).y1 = ry1 & proj(i,n).y2 = ry2 by PDIFF_1:def 1; proj(i,n).(y1 + y2) = proj(i,n).(yy1 + yy2) by REAL_NS1:2 .= (yy1 + yy2).i by PDIFF_1:def 1 .= ry1 + ry2 by RVSUM_1:11; hence thesis by A1; end; theorem Th38: for i be Nat, y1 be Point of REAL-NS n, r being Real holds proj(i,n).(r*y1) = r*(proj(i,n).y1) proof let i be Nat, y1 be Point of REAL-NS n, r be Real; reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def 4; reconsider y1i = yy1.i as Element of REAL by XREAL_0:def 1; proj(i,n).(r*y1) = proj(i,n).(r*yy1) by REAL_NS1:3 .= (r*yy1).i by PDIFF_1:def 1 .= r* y1i by RVSUM_1:44; hence thesis by PDIFF_1:def 1; end; theorem Th39: for g be PartFunc of REAL,REAL-NS n, x0 be Real, i be Nat st 1 <= i & i <= n & g is_differentiable_in x0 holds (proj(i,n)*g) is_differentiable_in x0 & proj(i,n).(diff(g,x0)) = diff((proj(i,n)*g),x0) proof let g be PartFunc of REAL,REAL-NS n, x0 be Real, i be Nat; assume A1: 1 <= i & i <= n & g is_differentiable_in x0; then consider N being Neighbourhood of x0 such that A2: N c= dom g & ex DFG be LinearFunc of REAL-NS n, GR be RestFunc of REAL-NS n st diff(g,x0) = DFG/.1 & for x be Real st x in N holds g/.x - g/.x0 = DFG/.(x-x0) + GR/.(x-x0) by NDIFF_3:def 4; consider DFG be LinearFunc of REAL-NS n, GR be RestFunc of REAL-NS n such that A3: diff(g,x0) = DFG/.1 & for x be Real st x in N holds g/.x - g/.x0 = DFG/.(x-x0) + GR/.(x-x0) by A2; consider LP be Point of REAL-NS n such that A4: for p be Real holds DFG/.p = p*LP by NDIFF_3:def 2; A5: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then reconsider PG = proj(i,n) as Function of REAL-NS n,REAL; the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then reconsider L = proj(i,n)*DFG as Function of REAL,REAL; A6: for r being Real holds L.r = (proj(i,n).LP)*r proof let r be Real; A7: dom L = REAL by FUNCT_2:def 1; dom DFG = REAL by FUNCT_2:def 1; then DFG.r = DFG/.r by XREAL_0:def 1,PARTFUN1:def 6 .= r*LP by A4; then proj(i,n).(DFG.r) = r*(proj(i,n).LP) by Th38; hence L.r = (proj(i,n).LP)*r by A7,FUNCT_1:12,XREAL_0:def 1; end; reconsider L as LinearFunc by A6,FDIFF_1:def 3; A8: GR is total by NDIFF_3:def 1; then reconsider FGR = GR as Function of REAL,REAL-NS n; A9: proj(i,n)*FGR is Function of REAL,REAL by A5; proj(i,n)*GR is RestFunc proof A10: dom GR = REAL by A8,PARTFUN1:def 2; reconsider R = proj(i,n)*GR as PartFunc of REAL,REAL; for r be Real st r > 0 ex d be Real st d > 0 & (for z be Real st z <> 0 & |.z.| < d holds (|.z.|" * |. R/.z .|) < r) proof let r be Real; assume r > 0; then consider d be Real such that A11: d > 0 & (for z be Real st z <> 0 & |.z.| < d holds (|.z.|"* ||. GR/.z .||) < r) by A8,NDIFF_4:23; take d; thus d> 0 by A11; let z be Real; assume A12: z <> 0 & |.z.| < d; A13: z in REAL by XREAL_0:def 1; A14: GR/.z = GR.z by A10,PARTFUN1:def 6,XREAL_0:def 1; A15: i in Seg n by A1; reconsider GRz = GR/.z as Point of REAL-NS n; reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4; reconsider GRzi = GRz1.i as Real; the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then dom proj(i,n) = the carrier of REAL-NS n by PARTFUN1:def 2; then A16: z in dom (proj(i,n)*GR) by A10,A14,FUNCT_1:11,A13; then A17: (proj(i,n)*GR).z = proj(i,n).(GR.z) by FUNCT_1:12 .= proj(i,n).(GRz1) by A10,A13,PARTFUN1:def 6; A18: |.GRzi.| <= ||. GR/.z .|| by A15,REAL_NS1:9; A19: 0 <= |.z.| by COMPLEX1:46; 0 <= |.GRzi.| by COMPLEX1:46; then A20: |.z.|"* |.GRzi.| <= |.z.|"* ||. GR/.z .|| by A18,A19,XREAL_1:66; |.z.|"* ||. GR/.z .|| < r by A11,A12; then A21: |.z.|"* |.GRzi.| < r by A20,XXREAL_0:2; reconsider Rz = (proj(i,n)*GR).z as Element of REAL by XREAL_0:def 1; |.z.|"* |. Rz .| < r by A21,PDIFF_1:def 1,A17; hence thesis by A16,PARTFUN1:def 6; end; hence thesis by A9,Th35; end; then reconsider R = proj(i,n)*GR as RestFunc; set pg = proj(i,n)*g; the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then dom proj(i,n) = the carrier of REAL-NS n by FUNCT_2:def 1; then rng g c= dom proj(i,n); then A22: dom g = dom (proj(i,n)*g) by RELAT_1:27; A23: for x be Real st x in N holds pg.x - pg.x0 = L.(x-x0) + R.(x-x0) proof let x be Real; reconsider xx = x as Element of REAL by XREAL_0:def 1; now assume A24: x in N; then A25: g/.x - g/.x0 = DFG/.(xx-x0) + GR/.(xx-x0) by A3; A26: x0 in N by RCOMP_1:16; A27: g/.x = g.x & g/.x0 = g.x0 by A2,A24,A26,PARTFUN1:def 6; reconsider PGSx = pg.x - pg.x0 as Element of REAL by XREAL_0:def 1; reconsider PGdx = pg.x as Element of REAL by XREAL_0:def 1; reconsider PGdx0 = pg.x0 as Element of REAL by XREAL_0:def 1; g.x in rng g by A2,A24,FUNCT_1:3; then reconsider Gx = g.x as Element of REAL n by REAL_NS1:def 4; g.x0 in rng g by A2,A26,FUNCT_1:3; then reconsider Gx0 = g.x0 as Element of REAL n by REAL_NS1:def 4; set projGx = proj(i,n).(g.x); reconsider projGx as Element of REAL by XREAL_0:def 1; set projGx0 = proj(i,n).(g.x0); reconsider projGx0 as Element of REAL by XREAL_0:def 1; reconsider Gx1 = Gx as Element of REAL-NS n by REAL_NS1:def 4; reconsider Gx01 = Gx0 as Element of REAL-NS n by REAL_NS1:def 4; reconsider Gsx = g/.x as Element of REAL n by REAL_NS1:def 4; reconsider Gsx0 = g/.x0 as Element of REAL n by REAL_NS1:def 4; reconsider dxx0 = x-x0 as Element of REAL by XREAL_0:def 1; reconsider Ldxx0 = L.(x-x0) as Element of REAL by XREAL_0:def 1; A28: dom R = REAL by A9,PARTFUN1:def 2; reconsider Rdxx0 = R.(x-x0) as Element of REAL by XREAL_0:def 1; reconsider Lxx0Rxx0 = L.(x-x0) + R.(x-x0) as Element of REAL by XREAL_0:def 1; reconsider Ldiff = DFG/.(x-x0) as Element of REAL n by REAL_NS1:def 4; set projLdiff = proj(i,n).Ldiff; reconsider projLdiff as Element of REAL; A29: dom GR = REAL by A8,PARTFUN1:def 2; then GR.dxx0 in rng GR by FUNCT_1:3; then reconsider Rdiff = GR.dxx0 as Element of REAL n by REAL_NS1:def 4; set projRdiff = proj(i,n).Rdiff; reconsider projRdiff as Element of REAL; dom DFG = REAL by FUNCT_2:def 1; then A30: Ldiff = DFG.(x-x0) by PARTFUN1:def 6,XREAL_0:def 1; dom L = REAL by FUNCT_2:def 1; then A31: L.(x-x0) = proj(i,n).Ldiff by FUNCT_1:12,XREAL_0:def 1,A30; A32: R.(x-x0) = proj(i,n).Rdiff by A28,FUNCT_1:12; A33: proj(i,n).Ldiff = Ldiff.i by PDIFF_1:def 1; A34: proj(i,n).Rdiff = Rdiff.i by PDIFF_1:def 1; reconsider diffGR = DFG/.(x-x0) + GR/.(x-x0) as Element of REAL n by REAL_NS1:def 4; reconsider Rsdiff = GR/.(x-x0) as Element of REAL n by REAL_NS1:def 4; PGSx = projGx - PGdx0 by A2,A22,A24,FUNCT_1:12 .= proj(i,n).Gx1 - proj(i,n).Gx01 by A2,A22,A26,FUNCT_1:12 .= Gx.i - proj(i,n).Gx01 by PDIFF_1:def 1 .= Gx.i - Gx0.i by PDIFF_1:def 1 .= (Gsx - Gsx0).i by A27,RVSUM_1:27 .= diffGR.i by A25,REAL_NS1:5 .= (Ldiff + Rsdiff).i by REAL_NS1:2 .= Ldiff.i + Rsdiff.i by RVSUM_1:11; hence thesis by A31,A33,A34,A29,PARTFUN1:def 6,A32; end; hence thesis; end; hence A35: proj(i,n)*g is_differentiable_in x0 by A2,A22; L.1 = 1*(proj(i,n).LP) by A6 .= proj(i,n).((1 qua Real) * LP) by RLVECT_1:def 8 .= proj(i,n).diff(g,x0) by A3,A4; hence proj(i,n).diff(g,x0) = diff((proj(i,n)*g),x0) by A35,A2,A22,A23,FDIFF_1:def 5; end; Lm7: for i be Nat holds proj(i,n).(0.(REAL-NS n)) = 0 proof let i be Nat; thus proj(i,n).(0.(REAL-NS n)) = proj(i,n).(0*n) by REAL_NS1:def 4 .= (0*n).i by PDIFF_1:def 1 .= 0; end; theorem Th40: for f be PartFunc of REAL,REAL-NS n, X be set st for i be Nat st 1 <= i & i <= n holds (proj(i,n)*f) | X is constant holds f| X is constant proof let f be PartFunc of REAL,REAL-NS n, X be set; assume A1: for i be Nat st 1 <= i & i <= n holds (proj(i,n)*f) | X is constant; A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4; now let x,y be object; assume A3: x in dom (f| X) & y in dom (f| X); then A4: x in dom f & x in X & y in dom f & y in X by RELAT_1:57; f.x in rng f by A4,FUNCT_1:3; then reconsider fx=f.x as Element of REAL n by REAL_NS1:def 4; f.y in rng f by A4,FUNCT_1:3; then reconsider fy=f.y as Element of REAL n by REAL_NS1:def 4; A5: len fy =n by CARD_1:def 7; A6: len fx =n by CARD_1:def 7; now let i be Nat; assume A7: 1 <= i & i <= len fx; dom proj(i,n) = the carrier of REAL-NS n by A2,FUNCT_2:def 1; then rng f c= dom proj(i,n); then A8: dom f = dom (proj(i,n)*f) by RELAT_1:27; A9: ((proj(i,n)*f) | X).x =((proj(i,n)*f)).x by A3,FUNCT_1:49 .= proj(i,n).(f.x) by A4,FUNCT_1:13 .= fx.i by PDIFF_1:def 1; A10: ((proj(i,n)*f) | X).y =((proj(i,n)*f)).y by A3,FUNCT_1:49 .= proj(i,n).(f.y) by A4,FUNCT_1:13 .= fy.i by PDIFF_1:def 1; A11: (proj(i,n)*f) | X is constant by A1,A7,A6; x in dom ((proj(i,n)*f) | X) & y in dom ((proj(i,n)*f) | X) by A8,A4,RELAT_1:57; hence fx.i = fy.i by A9,A10,A11,FUNCT_1:def 10; end; then A12: fx=fy by A5,CARD_1:def 7; thus (f| X).x = f.x by A3,FUNCT_1:49 .=(f| X).y by A3,A12,FUNCT_1:49; end; hence thesis by FUNCT_1:def 10; end; theorem Th41: for f be PartFunc of REAL,REAL-NS n st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n) holds f| (].a,b.[) is constant proof let f be PartFunc of REAL,REAL-NS n; assume A1: ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n); reconsider Z = ].a,b.[ as open Subset of REAL; now let i be Nat; assume A2: 1 <= i & i <= n; A3: now let x be Real; assume x in Z; then f is_differentiable_in x by A1,NDIFF_3:10; hence (proj(i,n)*f) is_differentiable_in x & proj(i,n).(diff(f,x)) = diff((proj(i,n)*f),x) by A2,Th39; end; A4: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; dom (proj(i,n)) = REAL n by FUNCT_2:def 1; then rng f c= dom (proj(i,n)) by A4; then A5: Z c= dom (proj(i,n)*f) by A1,RELAT_1:27; for x be Real st x in Z holds (proj(i,n)*f) is_differentiable_in x by A3; then A6: (proj(i,n)*f) is_differentiable_on ].a,b.[ by A5,FDIFF_1:9; for x be Real st x in ].a,b.[ holds diff((proj(i,n)*f),x) = 0 proof let x be Real; assume A7: x in ].a,b.[; then A8: proj(i,n).(diff(f,x)) = diff((proj(i,n)*f),x) by A3; diff(f,x) = 0.(REAL-NS n) by A1,A7; hence diff((proj(i,n)*f),x) = 0 by Lm7,A8; end; hence (proj(i,n)*f) | ].a,b.[ is constant by A6,ROLLE:7; end; hence thesis by Th40; end; theorem Th42: for f be continuous PartFunc of REAL,REAL-NS n st a < b & [.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,REAL-NS n; assume A1: a < b & [.a,b.] = dom f & f| (].a,b.[) is constant; A2: ].a,b.[ c= [.a,b.] by XXREAL_1:25; reconsider d = (b-a)/2 as Real; A3: 0 < b-a by A1,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 A1,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 REAL-NS n; A6: dom (f| (].a,b.[) ) = dom f /\ (].a,b.[) by RELAT_1:61 .= ].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; A10: a in dom f by A1; A11: b in dom f by A1; 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); A14: f is_continuous_in a by A10,NFCONT_3:def 2; 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; A18: 0 < d/(x+1) by A4,XREAL_1:139; 1 + (0 qua Real) <= 1 + x by XREAL_1:7; then A19: d/(x+1) <= d / 1 by XREAL_1:118,A3; A20: a + (0 qua Real) < a + d/(x+1) by A18,XREAL_1:8; a + d/(x+1) <= a + d by A19,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.[ by TARSKI:def 3; then A22: rng s1 c= dom f by A2,A1,XBOOLE_1:1; A23: now let p be Real; assume A24: 0

Function of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n), R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) means :Def7: for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n 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,REAL-NS n 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 '],REAL-NS n); 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,REAL-NS n such that A3: x=f0 & dom f0 = [' a,b '] by Def2; now let x0 be Real; assume A4: x0 in dom(G*f0); then x0 in dom f0 by FUNCT_1:11; then A5: f0 is_continuous_in x0 by NFCONT_3:def 2; the carrier of REAL-NS n = dom G by FUNCT_2:def 1; then G | (dom G ) is_continuous_in f0/.x0 by A1,NFCONT_1:def 7; hence G*f0 is_continuous_in x0 by A4,A5,NFCONT_3:15; end; then reconsider Gf = G*f0 as continuous PartFunc of REAL,REAL-NS n by NFCONT_3:def 2; dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then rng f0 c= dom G; 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,REAL-NS n such that A8: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4; set F = F0| ['a,b']; A9: dom F = dom F0 /\ ['a,b'] by RELAT_1:61 .= REAL /\ ['a,b'] by FUNCT_2:def 1 .= ['a,b'] by XBOOLE_1:28; A10: now let t be Real; assume A11: t in [.a,b.]; A12: t in REAL by XREAL_0:def 1; thus F.t = F0.t by A11,A9,A7,FUNCT_1:47 .= integral(Gf,a,t) by A8,A12; end; A13: for t be Real st t in [.a,b.] holds F is_continuous_in t by Th34,A6,A1,A9,A10; set G0 = REAL --> y0; set G1 = G0| ['a,b']; A14: dom G1 = dom G0 /\ ['a,b'] by RELAT_1:61 .= REAL /\ ['a,b'] by FUNCT_2:def 1 .= ['a,b'] by XBOOLE_1:28; A15: now let t be Real; assume A16: t in [.a,b.]; thus G1.t = G0.t by A16,A14,A7,FUNCT_1:47 .= y0 by XREAL_0:def 1,FUNCOP_1:7; end; A17: F is continuous by A7,A9,A13,NFCONT_3:def 2; set g=G1+F; A18: dom g = dom F /\ dom G1 by VFUNCT_1:def 1 .= ['a,b'] by A9,A14; reconsider g as continuous PartFunc of REAL,REAL-NS n by A17; reconsider y=g as Element of D by A18,Def2; take y; now let t be Real; assume A19:t in ['a,b']; A20: G1/.t = G1.t by A19,A14,PARTFUN1:def 6 .= y0 by A19,A7,A15; A21: F/.t = F.t by A19,A9,PARTFUN1:def 6 .= integral(Gf,a,t) by A19,A7,A10; thus g.t = g/.t by A18,A19,PARTFUN1:def 6 .= y0 + integral(Gf,a,t) by A20,A21,A18,A19,VFUNCT_1:def 1; end; hence thesis by A18,A3; end; consider F being Function of D,D such that A22: for x being Element of D holds P[x,F.x] from FUNCT_2:sch 3 (A2); take F; thus thesis by A22; end; uniqueness proof let F1,F2 be Function of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n), R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); assume A23: for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) holds ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n 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 A24: for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) holds ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n 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 '],REAL-NS n); consider f1,g1,Gf1 be continuous PartFunc of REAL,REAL-NS n such that A25: 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 A23; consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n such that A26: 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 A24; now let t be object; assume A27: t in dom g1; then reconsider t0=t as Real; thus g1.t = y0+ integral(Gf2,a,t0) by A26,A27,A25 .= g2.t by A27,A26,A25; end; hence F1.x = F2.x by A25,A26,FUNCT_1:2; end; hence F1=F2 by FUNCT_2:def 8; end; end; theorem Th49: a <= b & 0 < r & (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) implies for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n), g,h be continuous PartFunc of REAL,REAL-NS n 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 REAL-NS n holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; A2: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; for x1,x2 be Point of REAL-NS n st x1 in (the carrier of REAL-NS n) & x2 in (the carrier of REAL-NS n) holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then G is_Lipschitzian_on the carrier of (REAL-NS n) by A1,A2,NFCONT_1:def 9; 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 '],REAL-NS n), g,h be continuous PartFunc of REAL,REAL-NS n; 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,REAL-NS n 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 Def7,A1,A3; consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n 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 Def7,A1,A3; set Gf12= Gf1 - Gf2; A7: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then rng f1 c= dom G; then A8: dom Gf1 =[' a,b '] by A5,RELAT_1:27; rng f2 c= dom G by A7; then A9: dom Gf2 =[' a,b '] by A6,RELAT_1:27; reconsider Gf12 as continuous PartFunc of REAL,REAL-NS n; A10: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; 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; A13: dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2 .= ['a,b'] by A8,A9; A14: Gf12 is_integrable_on ['a,b'] by A13,Th33; A15: Gf12| ['a,b'] is bounded by A13,Th32; Gf12| (['a,b']) is continuous; then A16: (||. Gf12 .||) | [' a,b '] is continuous by A13,NFCONT_3:22; [' a,b '] = dom (||. Gf12 .||) by A13,NORMSP_0:def 2; then A17: (||. Gf12 .||) is_integrable_on [' a,b '] by A16,INTEGRA5:11; A18: a in ['a,b'] by A10,A1; 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']; A20: ['a,t'] c= [' a,b '] by A12,INTEGR19:1; A21: Gf12/.x =Gf1/.x -Gf2/.x by A13,A20,A19,VFUNCT_1:def 2; 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; A23: Gf2/.x = (Gf2).x by A9,A20,A19,PARTFUN1:def 6 .= G.(f2.x) by A20,A19,A9,A6,FUNCT_1:12 .= G/.(f2/.x) by A20,A19,A6,PARTFUN1:def 6; A24: ||. Gf1/.x -Gf2/.x .||<=r*||.(f1/.x)-(f2/.x).|| by A22,A23,A1; ||.(f1/.x)-(f2/.x).|| <=||.u-v.|| by A20,A19,A5,A6,Th26; then r*||.(f1/.x)-(f2/.x).|| <=r*||.u-v.|| by A1,XREAL_1:64; hence thesis by A21,A24,XXREAL_0:2; end; then A25: ||. integral(Gf12,a,t) .||<= ((r*||.u-v.|| ))* (t-a) by Th45,A1,A17,A14,A15,A13,A18,A11,A12; A26: Gf1 is_integrable_on ['a,b'] by A8,Th33; A27: Gf1| ['a,b'] is bounded by A8,Th32; A28: Gf2 is_integrable_on ['a,b'] by A9,Th33; A29: Gf2| ['a,b'] is bounded by A9,Th32; A30: integral(Gf12,a,t) = integral(Gf1,a,t) - integral(Gf2,a,t) by A8,A9,A26,A27,A28,A29,A18,A11,A1,INTEGR19:50; A31: g/.t = g1.t by A4,A11,A5,PARTFUN1:def 6 .= y0 + integral(Gf1,a,t) by A5,A11; A32: h/.t = g2.t by A4,A11,A6,PARTFUN1:def 6 .= y0 + integral(Gf2,a,t) by A6,A11; g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by A31,A32,RLVECT_1:27 .= ( integral(Gf1,a,t) + (y0 - y0) ) -integral(Gf2,a,t) by RLVECT_1:28 .= ( integral(Gf1,a,t) + 0.(REAL-NS n) ) -integral(Gf2,a,t) by RLVECT_1:15 .= integral(Gf12,a,t) by A30; hence thesis by A25; end; theorem Th50: a <= b & 0 < r & (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) implies for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n), m be Element of NAT, g,h be continuous PartFunc of REAL,REAL-NS n 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 REAL-NS n holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; set F = Fredholm(G,a,b,y0); A2: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; for x1,x2 be Point of REAL-NS n st x1 in (the carrier of REAL-NS n) & x2 in (the carrier of REAL-NS n) holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then G is_Lipschitzian_on the carrier of (REAL-NS n) by A1,A2,NFCONT_1:def 9; 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 '],REAL-NS n); defpred P[Nat] means for g,h be continuous PartFunc of REAL,REAL-NS n 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,REAL-NS n; assume A5: g = iter(F,( (0 qua Element of NAT ) + 1)).u1 & h = iter(F,( (0 qua Element of NAT ) + 1)).v1; A6: g= F.u1 by A5,FUNCT_7:70; A7: h= F.v1 by A5,FUNCT_7:70; now let t be Real; assume t in [' a,b ']; then ||. g/.t - h/.t .|| <= r*(t-a) * ||.u1-v1.|| by Th49,A1,A6,A7; 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,REAL-NS n; assume A10: g = iter(F,((k+1)+1)).u1 & h = iter(F,((k+1)+1)).v1; reconsider u=iter(F,(k+1)).u1 as VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); reconsider v=iter(F,(k+1)).v1 as VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); A11: dom(iter(F,k+1)) = the carrier of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) 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,REAL-NS n 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 Def7,A1,A3; consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n 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 Def7,A1,A3; set Gf12= Gf1 - Gf2; A16: for t be Real st t in [' a,b '] holds ||. f1/.t - f2/.t .|| <= ( (r*(t-a))|^(k+1) )/((k+1)!) * ||.u1-v1.|| by A9,A14,A15; A17: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then rng f1 c= dom G; then A18: dom Gf1 =[' a,b '] by A14,RELAT_1:27; rng f2 c= dom G by A17; then A19: dom Gf2 =[' a,b '] by A15,RELAT_1:27; reconsider Gf12 as continuous PartFunc of REAL,REAL-NS n; 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; A23: ex g be Element of REAL st t=g & a<=g & g <= b proof consider g be Real such that A24: 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 A24; end; A25: dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2 .= ['a,b'] by A18,A19; then A26: dom (||. Gf12 .||) = ['a,b'] by NORMSP_0:def 2; A27: Gf12 is_integrable_on ['a,b'] by A25,Th33; A28: Gf12| ['a,b'] is bounded by A25,Th32; A29: a in ['a,b'] by A20,A1; Gf12 | ['a,b'] is continuous; then A30: (||. Gf12 .||) | [' a,b '] is continuous by A25,NFCONT_3:22; [' a,b '] = dom (||. Gf12 .||) by A25,NORMSP_0:def 2; then A31: ||. Gf12 .|| is_integrable_on [' a,b '] by A30,INTEGRA5:11; min(a,t) = a & max(a,t) = t by A22,XXREAL_0:def 9,def 10; then A32: ||. Gf12 .|| is_integrable_on ['a,t'] & (||. Gf12 .||) | ['a,t'] is bounded & ||. integral(Gf12,a,t) .|| <= integral((||. Gf12 .||),a,t) by A1,A27,A28,A25,A29,A21,A31,Th44; A33: k+1 is non zero Element of NAT by ORDINAL1:def 12; consider rg be PartFunc of REAL,REAL such that A34: 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 Lm12,A23,A33; A35: ['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 A36: x in ['a,t']; A37: Gf12/.x =Gf1/.x -Gf2/.x by A25,A35,A36,VFUNCT_1:def 2; A38: Gf1/.x = (Gf1).x by A18,A35,A36,PARTFUN1:def 6 .= G.(f1.x) by A35,A36,A18,A14,FUNCT_1:12 .= G/.(f1/.x) by A35,A36,A14,PARTFUN1:def 6; A39: Gf2/.x = (Gf2).x by A19,A35,A36,PARTFUN1:def 6 .= G.(f2.x) by A35,A36,A19,A15,FUNCT_1:12 .= G/.(f2/.x) by A35,A36,A15,PARTFUN1:def 6; A40: ||. Gf1/.x -Gf2/.x .|| <= r*||.(f1/.x)-(f2/.x).|| by A38,A39,A1; r*||.(f1/.x)-(f2/.x).|| <=r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.||) by A1,XREAL_1:64,A16,A35,A36; then r*||.(f1/.x)-(f2/.x).|| <=rg.x by A36,A34; then ||. Gf1/.x -Gf2/.x .|| <=rg.x by A40,XXREAL_0:2; hence thesis by A26,A35,A36,NORMSP_0:def 2,A37; end; then A41: integral((||. Gf12 .||),a,t) <= integral(rg,a,t) by A32,A22,A26,A35,A34,Th48; A42: Gf1 is_integrable_on ['a,b'] by A18,Th33; A43: Gf1| ['a,b'] is bounded by A18,Th32; A44: Gf2 is_integrable_on ['a,b'] by A19,Th33; A45: Gf2| ['a,b'] is bounded by A19,Th32; A46: integral(Gf12,a,t) = integral(Gf1,a,t) - integral(Gf2,a,t) by A18,A19,A42,A43,A44,A45,A29,A21,A1,INTEGR19:50; A47: g/.t = g1.t by A12,A10,A21,A14,PARTFUN1:def 6 .= y0+ integral(Gf1,a,t) by A14,A21; A48: h/.t = g2.t by A13,A10,A21,A15,PARTFUN1:def 6 .= y0+ integral(Gf2,a,t) by A15,A21; g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by RLVECT_1:27,A47,A48 .= ( integral(Gf1,a,t) + (y0 - y0) ) -integral(Gf2,a,t) by RLVECT_1:28 .= ( integral(Gf1,a,t) + 0.(REAL-NS n) ) -integral(Gf2,a,t) by RLVECT_1:15 .= integral(Gf12,a,t) by A46; hence thesis by A41,A32,XXREAL_0:2,A34; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A8); hence thesis; end; Lm13: 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; Lm14: 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 A2: s is convergent & lim s = 0 by SERIES_1:4; consider n be Nat such that A3: for m be Nat st n<=m holds |.s.m- 0 .| < 1 by A2,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 Th51: for m be Nat st a <= b & 0 < r & (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) holds for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) 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 REAL-NS n holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||; let u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); reconsider u1=iter(Fredholm(G,a,b,y0),(m+1)).u as VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); reconsider v1=iter(Fredholm(G,a,b,y0),(m+1)).v as VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n); consider g be continuous PartFunc of REAL,REAL-NS n such that A2: u1=g & dom g = [' a,b '] by Def2; consider h be continuous PartFunc of REAL,REAL-NS n such that A3: v1=h & dom h = [' a,b '] by Def2; 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,Th50,A1,A2,A3; ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A6,A1,Lm13; hence ||. g/.t - h/.t .|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A7,XXREAL_0:2; end; hence thesis by Th27,A2,A3; end; theorem Th52: a