0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r by A9,A16,A19; end; now assume A21: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; now let s be 0-convergent non-zero Real_Sequence; A22: s is convergent & lim s = 0; A23: now let r be Real; assume r > 0; then consider d be Real such that A24: d > 0 and A25: for z be Real st z <> 0 & |.z.| < d holds |.z.|"* ||. R/.z .|| < r by A21; consider n0 be Nat such that A26: for m be Nat st n0 <=m holds |. s.m-0 .| < d by A22,A24,SEQ_2:def 7; take n0; thus for m be Nat st n0 <=m holds ||. ((s")(#)(R/*s)).m- 0.S .|| < r proof A27: rng s c= dom R by A1; let m be Nat; assume n0 <=m; then A28: |. s.m-0 .| < d by A26; A30: m in NAT by ORDINAL1:def 12; |. s.m .|" * ||. R/.(s.m) .|| = |.(s.m)".| * ||. R/.(s.m) .|| by COMPLEX1:66 .= ||. (s.m)"*(R/.(s.m)) .|| by NORMSP_1:def 1 .= ||. (s.m)"*((R/*s).m) .|| by A27,FUNCT_2:109,A30 .= ||. (s".m)*((R/*s).m) .|| by VALUED_1:10 .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2 .= ||. ((s")(#)(R/*s)).m- 0.S .|| by RLVECT_1:13; hence thesis by A25,A28,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.S by A23,NORMSP_1:def 7; end; hence R is RestFunc-like by NDIFF_3:def 1; end; hence thesis by A2; end; theorem Th2: for R be RestFunc of S st R/.0=0.S for e be Real st e > 0 ex d be Real st d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.| proof let R be RestFunc of S such that A1: R/.0=0.S; let e be Real such that A2: e > 0; R is total by NDIFF_3:def 1; then consider d be Real such that A3: d > 0 and A4: for z be Real st z <> 0 & |.z.| < d holds |.z.|"* ||. R/.z .|| < e by A2,Th1; take d; now let h be Real such that A5: |.h.| < d; A6: 0 <= |.h.| by COMPLEX1:46; per cases; suppose A7: h <> 0; then |.h.|"*||. R/.h .|| <= e by A4,A5; then |.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by A6,XREAL_1:64; then A8: |.h.|*|.h.|"*||. R/.h .|| <= e * |.h.|; |.h.| <> 0 by A7,COMPLEX1:45; then 1*||. R/.h .|| <= e * |.h.| by A8,XCMPLX_0:def 7; hence ||. R/.h .|| <= e* |.h.|; end; suppose A9: h = 0; reconsider p0=0 as Real; p0* |.h.| <= e* |.h.| by A2,A6; hence ||. R/.h .|| <= e* |.h.| by A1,A9; end; end; hence thesis by A3; end; theorem Th3: for R be RestFunc of S for L be Lipschitzian LinearOperator of S,T holds L*R is RestFunc of T proof let R be RestFunc of S; let L be Lipschitzian LinearOperator of S,T; consider K be Real such that A1: 0 <= K and A2: for z be Point of S holds ||. L.z .|| <= K * ||.z.|| by LOPBAN_1:def 8; dom L = the carrier of S by FUNCT_2:def 1; then A3:rng R c= dom L; A4:R is total by NDIFF_3:def 1; then A5:dom R = REAL by PARTFUN1:def 2; now let e be Real such that A6: e > 0; set e1 = e/2/(1 + K); consider d be Real such that A7: 0 < d and A8: for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||. R/.h .|| < e1 by A1,A4,A6,Th1; A9: e/2 < e by A6,XREAL_1:216; now let h be Real; reconsider hh=h as Element of REAL by XREAL_0:def 1; assume A10: h <> 0 & |.h.| < d; then |.h.|"* ||.(R/.h).|| < e1 by A8; then (K +1)*(|.h.|"* ||.R/.h.||) <= (K +1)*e1 by A1,XREAL_1:64; then A11: (K +1)*(|.h.|"* ||.R/.h.||) <= e/2 by A1,XCMPLX_1:87; |.h.| <> 0 by A10,COMPLEX1:45; then A12: |.h.| > 0 by COMPLEX1:46; reconsider p0=0, p1=1 as Element of REAL by XREAL_0:def 1; p0 + K < p1 + K by XREAL_1:8; then A13: K * ||.R/.h.|| <= (K +1) * ||.R/.h.|| by XREAL_1:64; ||.L.(R/.h).|| <= K * ||.R/.h.|| by A2; then ||.L.(R/.h).|| <= (K +1) * ||.R/.h.|| by A13,XXREAL_0:2; then |.h.|"* ||.L.(R/.h).|| <= |.h.|"*((K +1)*||. R/.h .||) by A12,XREAL_1:64 ; then A14: |.h.|"* ||.L.(R/.h).|| <= e/2 by A11,XXREAL_0:2; L.(R/.h) = L/.(R/.h); then L.(R/.hh) =(L*R)/.hh by A5,A3,PARTFUN2:5; hence |.h.|"* ||.(L*R)/.h.|| < e by A9,A14,XXREAL_0:2; end; hence ex d be Real st d > 0 & for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||.(L*R)/.h.|| < e by A7; end; hence thesis by A4,Th1; end; theorem Th4: for R1 be RestFunc of S st R1/.0 = 0.S for R2 be RestFunc of S,T st R2/.(0.S) = 0.T for L be LinearFunc of S holds R2*(L+R1) is RestFunc of T proof let R1 be RestFunc of S; assume R1/.0 = 0.S; then consider d0 be Real such that A1: 0 < d0 and A2: for h be Real st |.h.| < d0 holds ||.R1/.h.|| <= 1* |.h.| by Th2; let R2 be RestFunc of S,T such that A3:R2/.(0.S) = 0.T; let L be LinearFunc of S; consider r be Point of S such that A4: for h be Real holds L/.h = h*r by NDIFF_3:def 2; reconsider K = ||.r.|| as Real; R2 is total by NDIFF_1:def 5; then dom R2 = the carrier of S by PARTFUN1:def 2; then A5:rng(L+R1) c= dom R2; R1 is total by NDIFF_3:def 1; then L+R1 is total by VFUNCT_1:32; then A6:dom(L+R1) = REAL by PARTFUN1:def 2; then dom(R2*(L+R1)) = REAL by A5,RELAT_1:27; then A7:R2*(L+R1) is total by PARTFUN1:def 2; now let e be Real such that A8: e > 0; A9: e/2 < e by A8,XREAL_1:216; set e1 = e/2/(1 + K); consider d be Real such that A10: 0 < d and A11: for z be Point of S st ||.z.|| < d holds ||.R2/.z.|| <= e1*||.z.|| by A3,A8,NDIFF_2:7; set d1 = d/(1 + K); set dd1 = min(d0,d1); A12: dd1 <= d1 & dd1 <= d0 by XXREAL_0:17; A13: now let hh be Real such that A14: hh <> 0 and A15: |.hh.| < dd1; reconsider h=hh as Element of REAL by XREAL_0:def 1; |.h.| < d0 by A12,A15,XXREAL_0:2; then A16: ||.R1/.h.|| <=1* |.h.| by A2; reconsider p0=0 as Element of REAL by XREAL_0:def 1; L.h = L/.h .= h*r by A4; then ||. L.h .|| - K * |.h.| + K * |.h.| <= p0 + K * |.h.| by NORMSP_1:def 1; then ||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.|| & ||.L.h.|| + ||. R1/.h .|| <= K * |.h.| + 1 * |.h.| by A16,NORMSP_1:def 1,XREAL_1:7; then A17: ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2; then A18: e1 * ||. L.h+R1/.h .|| <= e1*((K +1)*|.h.|) by A8,XREAL_1:64; |.h.| < d1 by A12,A15,XXREAL_0:2; then (K +1) * |.h.| < (K +1) * d1 by XREAL_1:68; then ||. L.h+R1/.h .|| < (K +1) * d1 by A17,XXREAL_0:2; then ||. L.h+R1/.h.|| < d by XCMPLX_1:87; then ||. R2/.(L.h+R1/.h) .|| <= e1 * ||. L.h+R1/.h .|| by A11; then A19: ||. R2/.(L.h+R1/.h) .|| <= e1*((K +1)*|.h.|) by A18,XXREAL_0:2; A20: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h) .=R2/.((L+R1)/.h) by A6,VFUNCT_1:def 1 .=(R2*(L+R1))/.h by A6,A5,PARTFUN2:5; A21: |.h.| <> 0 by A14,COMPLEX1:45; then |.h.| > 0 by COMPLEX1:46; then |.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* (K +1) * |.h.|) by A20,A19,XREAL_1:64; then |.h.|"* ||. (R2*(L+R1))/.h .|| <= |.h.|*|.h.|"*e1*(K +1); then |.h.|"* ||. (R2*(L+R1))/.h .|| <= 1 * e1 * (K +1) by A21,XCMPLX_0:def 7; then |.h.|"* ||. (R2*(L+R1))/.h .|| <= e/2 by XCMPLX_1:87; hence |.hh.|"* ||.(R2*(L+R1))/.hh.|| < e by A9,XXREAL_0:2; end; 0 < dd1 by A1,A10,XXREAL_0:15; hence ex dd1 be Real st dd1 > 0 & for h be Real st h <> 0 & |.h.| < dd1 holds |.h.|"* ||. (R2*(L+R1))/.h .|| < e by A13; end; hence thesis by A7,Th1; end; theorem Th5: for R1 be RestFunc of S st R1/.0=0.S for R2 be RestFunc of S,T st R2/.(0.S)=0.T for L1 be LinearFunc of S for L2 be Lipschitzian LinearOperator of S,T holds L2*R1 + R2*(L1+R1) is RestFunc of T proof let R1 be RestFunc of S such that A1: R1/.0=0.S; let R2 be RestFunc of S,T such that A2: R2/.(0.S)=0.T; let L1 be LinearFunc of S; let L2 be Lipschitzian LinearOperator of S,T; L2*R1 is RestFunc of T & R2*(L1+R1) is RestFunc of T by A1,A2,Th4,Th3; hence thesis by NDIFF_3:7; end; reconsider jj=1 as Element of REAL by XREAL_0:def 1; theorem Th6: for x0 be Real for g be PartFunc of REAL,the carrier of S st g is_differentiable_in x0 for f be PartFunc of the carrier of S,the carrier of T st f is_differentiable_in (g/.x0) holds f*g is_differentiable_in x0 & diff(f*g,x0) = diff(f,g/.x0).diff(g,x0) proof let x0 be Real; let g be PartFunc of REAL,the carrier of S such that A1: g is_differentiable_in x0; consider N1 being Neighbourhood of x0 such that A2: N1 c= dom g and A3: ex L1 be LinearFunc of S,R1 be RestFunc of S st diff(g,x0) = L1/.1 & for x be Real st x in N1 holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A1,NDIFF_3:def 4; let f be PartFunc of the carrier of S,the carrier of T; assume f is_differentiable_in g/.x0; then consider N2 being Neighbourhood of g/.x0 such that A4: N2 c= dom f and A5: ex R2 be RestFunc of S,T st R2/.(0.S) = 0.T & R2 is_continuous_in 0.S & for y be Point of S st y in N2 holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by NDIFF_1:47; consider R2 be RestFunc of S,T such that A6: R2/.0.S=0.T and A7: for y be Point of S st y in N2 holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by A5; reconsider L2 = diff(f,g/.x0) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9; consider L1 be LinearFunc of S,R1 be RestFunc of S such that A8: diff(g,x0) = L1/.1 & for x be Real st x in N1 holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A3; consider r be Point of S such that A9: for p be Real holds L1/.p = p*r by NDIFF_3:def 2; reconsider p0=0 as Element of REAL by XREAL_0:def 1; g/.x0-g/.x0 = L1/.(x0-x0) + R1/.(x0-x0) by A8,RCOMP_1:16; then 0.S = L1/.0 + R1/.0 by RLVECT_1:15; then 0.S = p0*r + R1/.0 by A9; then 0.S = 0.S + R1/.0 by RLVECT_1:10; then R1/.0 = 0.S by RLVECT_1:4; then reconsider R0=L2*R1+R2*(L1+R1) as RestFunc of T by A6,Th5; A10: dom(L2*L1) = REAL by FUNCT_2:def 1; reconsider q = L2.r as Point of T; now let pp be Real; reconsider p=pp as Element of REAL by XREAL_0:def 1; L2.(L1/.p) = L2.(p*r) by A9; then L2.(L1/.p) = p*q by LOPBAN_1:def 5; then (L2*L1).p = p*q by A10,FUNCT_1:12; hence (L2*L1)/.pp = pp*q by A10,PARTFUN1:def 6; end; then reconsider L0=L2*L1 as LinearFunc of T by NDIFF_3:def 2; g is_continuous_in x0 by A1,NDIFF_3:22; then consider N3 be Neighbourhood of x0 such that A11: g.:N3 c= N2 by NFCONT_3:10; consider N be Neighbourhood of x0 such that A12: N c= N1 and A13: N c= N3 by RCOMP_1:17; A14: dom L2 = the carrier of S by FUNCT_2:def 1; then A15: rng R1 c= dom L2; A16: rng L1 c= dom L2 by A14; now let x be object; assume A17: x in N; then reconsider x9 = x as Real; A18: x in N1 by A12,A17; then g.x9 in g.:N3 by A2,A13,A17,FUNCT_1:def 6; then g.x9 in N2 by A11; hence x in dom(f*g) by A2,A4,A18,FUNCT_1:11; end; then A19: N c= dom(f*g); A20: now let x be Real such that A21: x in N; A22: g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A8,A12,A21; x in N1 by A12,A21; then g.x in g.:N3 by A2,A13,A21,FUNCT_1:def 6; then g.x in N2 by A11; then A24: g/.x in N2 by A2,A12,A21,PARTFUN1:def 6; A25: x0 in N by RCOMP_1:16; A26: R1 is total by NDIFF_3:def 1; then A27: dom R1 = REAL by PARTFUN1:def 2; A28: dom(L2*R1) = REAL by A26,PARTFUN1:def 2; L1+R1 is total by A26,VFUNCT_1:32; then A29: dom(L1+R1)=REAL by PARTFUN1:def 2; R2 is total by NDIFF_1:def 5; then dom R2 = the carrier of S by PARTFUN1:def 2; then A30: rng (L1+R1) c= dom R2; then dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27; then A31: dom (L2*R1+R2*(L1+R1)) = REAL /\ REAL by A28,A29,VFUNCT_1:def 1; reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1; L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0)); then A32: L2.(R1/.(x-x0)) =(L2*R1)/.(dxx0) by A27,A15,PARTFUN2:5; A33: R2/.(L1/.(x-x0)+R1/.(x-x0)) =R2/.((L1+R1)/.(dxx0)) by A29,VFUNCT_1:def 1 .=(R2*(L1+R1))/.(dxx0) by A29,A30,PARTFUN2:5; A34: dom L1 = REAL by FUNCT_2:def 1; A35: (L2*L1)/.(x-x0) = L2/.(L1/.(dxx0)) by PARTFUN2:5,A34,A16; thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A19,A21,PARTFUN2:3 .=f/.(g/.x) -f/.(g/.x0) by A19,A25,PARTFUN2:3 .=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A24 .=L2.(L1/.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A22,A33, VECTSP_1:def 20 .=L2.(L1/.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A32, RLVECT_1:def 3 .=L0/.(x-x0) + R0/.(x-x0) by A35,A31,VFUNCT_1:def 1; end; hence A36: f*g is_differentiable_in x0 by A19,NDIFF_3:def 3; dom L1 = REAL by FUNCT_2:def 1; then (L2*L1)/.1 = L2/.(L1/.jj) by PARTFUN2:5,A16 .= diff(f,g/.x0).diff(g,x0) by A8; hence thesis by A36,A19,A20,NDIFF_3:def 4; end; theorem Th7: for S be RealNormSpace, xseq be FinSequence of S, yseq be FinSequence of REAL st len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ) holds ||.Sum xseq.|| <= Sum yseq proof let S be RealNormSpace, xseq be FinSequence of S, yseq be FinSequence of REAL; assume that A1: len xseq = len yseq and A2: for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .||; defpred P[Nat] means for xseq be FinSequence of S, yseq be FinSequence of REAL st $1=len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ) holds ||.Sum xseq.|| <= Sum yseq; A3:P[0] proof let xseq be FinSequence of S, yseq be FinSequence of REAL; assume A4: 0 = len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ); consider Sx be sequence of the carrier of S such that A5: Sum xseq = Sx.(len xseq) & Sx.0 = 0.S & for j be Nat, v be Element of S st j < len xseq & v = xseq.(j+1) holds Sx.(j+1) = Sx.j + v by RLVECT_1:def 12; yseq = {} by A4; hence thesis by A4,A5,RVSUM_1:72; end; A6:now let i be Nat; assume A7: P[i]; now let xseq be FinSequence of S, yseq be FinSequence of REAL; set xseq0=xseq|i, yseq0=yseq|i; assume A8: i+1=len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ); A9: for k be Element of NAT st k in dom xseq0 holds yseq0.k = ||. xseq0/.k .|| proof let k be Element of NAT; assume A10: k in dom xseq0; then A11: k in Seg i & k in dom xseq by RELAT_1:57; then A12: yseq.k = ||. xseq/.k .|| by A8; xseq/.k = xseq.k by A11,PARTFUN1:def 6; then xseq/.k = xseq0.k by A11,FUNCT_1:49; then xseq/.k = xseq0/.k by A10,PARTFUN1:def 6; hence thesis by A11,A12,FUNCT_1:49; end; A13: dom xseq = Seg(i+1) by A8,FINSEQ_1:def 3; then A14: yseq.(i+1) = ||. xseq/.(i+1) .|| by A8,FINSEQ_1:4; A15: 1 <= i + 1 by NAT_1:11; yseq = (yseq|i)^<*yseq/.(i+1) *> by A8,FINSEQ_5:21; then yseq = yseq0 ^<*(yseq.(i+1))*> by A8,A15,FINSEQ_4:15; then A16: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74; reconsider v = xseq.(len xseq) as Element of S by A13,A8,FINSEQ_1:4,PARTFUN1:4; A18: v = xseq/.(i+1) by A8,A13,FINSEQ_1:4,PARTFUN1:def 6; A19: i=len xseq0 by A8,FINSEQ_1:59,NAT_1:11; then xseq0 = xseq| (dom xseq0) by FINSEQ_1:def 3; then A20: Sum xseq = Sum xseq0 + v by A8,A19,RLVECT_1:38; A21: ||. Sum xseq0 + v.|| <= ||.Sum xseq0 .|| + ||. v .|| by NORMSP_1:def 1; len xseq0 = len yseq0 by A8,A19,FINSEQ_1:59,NAT_1:11; then ||. Sum xseq0 .|| + ||.v.|| <= Sum yseq0 + yseq.(i+1) by A7,A9,A19,A14,A18,XREAL_1:6; hence ||. Sum xseq .|| <= Sum yseq by A16,A20,A21,XXREAL_0:2; end; hence P[i+1]; end; for i be Nat holds P[i] from NAT_1:sch 2(A3,A6); hence thesis by A1,A2; end; theorem Th8: for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds N1/\ N2 is Neighbourhood of x proof let S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x; consider N be Neighbourhood of x such that A1: N c= N1 & N c= N2 by NDIFF_1:1; A2:N c= N1/\ N2 by A1,XBOOLE_1:19; consider g be Real such that A3: 0 < g and A4: {y where y is Point of S: ||.y-x .|| < g} c= N by NFCONT_1:def 1; {y where y is Point of S: ||.y-x .|| < g} c= N1 /\ N2 by A2,A4; hence thesis by A3,NFCONT_1:def 1; end; theorem Th9: for X be non-empty FinSequence, x be set st x in product X holds x is FinSequence proof let X be non-empty FinSequence, x be set; assume x in product X; then consider g be Function such that A1: x = g & dom g = dom X & for i be object st i in dom X holds g.i in X.i by CARD_3:def 5; dom g = Seg len X by A1,FINSEQ_1:def 3; hence x is FinSequence by A1,FINSEQ_1:def 2; end; registration let G be RealNormSpace-Sequence; cluster product G -> constituted-FinSeqs; coherence proof let a be Element of product G; product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hence thesis by Th9; end; end; Lm1: now let G be RealLinearSpace-Sequence; len carr G = len G by PRVECT_2:def 4; hence dom carr G = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; end; definition let G be RealLinearSpace-Sequence; let z be Element of product carr G; let j be Element of dom G; redefine func z.j -> Element of G.j; correctness proof reconsider zz=z as FinSequence by Th9; dom carr G = dom G by Lm1; then zz.j in carr G.j by CARD_3:9; hence thesis by PRVECT_2:def 4; end; end; theorem Th10: the carrier of product G = product carr G proof product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hence thesis; end; theorem Th11: for i be Element of dom G, r be set, x be Function st r in the carrier of (G.i) & x in product carr G holds x +* (i,r) in the carrier of product G proof let i be Element of dom G, r be set, x be Function; assume A1: r in the carrier of (G.i) & x in product carr G; then consider g be Function such that A2: x = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; set h = x +* (i,r); set s = i .--> r; s = {i} --> r by FUNCOP_1:def 9; then A3:dom s = {i} by FUNCOP_1:13; A4:dom h = dom carr G by A2,FUNCT_7:30; for j be object st j in dom carr G holds h.j in (carr G).j proof let j be object; assume A5: j in dom carr G; per cases; suppose not j in dom s; then j <> i by A3,TARSKI:def 1; then h.j = x.j by FUNCT_7:32; hence h.j in (carr G).j by A2,A5; end; suppose j in dom s; then A6: j = i by TARSKI:def 1; then h.j = r by A5,A2,FUNCT_7:31; hence h.j in (carr G).j by A1,A6,PRVECT_2:def 4; end; end; then x +* (i,r) in product carr G by A4,CARD_3:def 5; hence thesis by Th10; end; definition let G be RealNormSpace-Sequence; attr G is non-trivial means :Def1: for j be Element of dom G holds G.j is non trivial; end; registration cluster non-trivial for RealNormSpace-Sequence; correctness proof take G = <* the non trivial RealNormSpace *>; let j be Element of dom G; dom G = Seg 1 by FINSEQ_1:38; then j = 1 by FINSEQ_1:2,TARSKI:def 1; hence thesis by FINSEQ_1:40; end; end; registration let G be non-trivial RealNormSpace-Sequence; let i be Element of dom G; cluster G.i -> non trivial for RealNormSpace; correctness by Def1; end; registration let G be non-trivial RealNormSpace-Sequence; cluster product G -> non trivial; correctness proof A1:the carrier of product G = product carr G by Th10; not for x,y be set st x in product carr G & y in product carr G holds x = y proof assume A2: for x,y be set st x in product carr G & y in product carr G holds x = y; consider z be object such that A3: z in product carr G by XBOOLE_0:def 1; consider g be Function such that A4: z = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by A3,CARD_3:def 5; set i = the Element of dom G; now let r,s be object; assume A5: r in the carrier of (G.i) & s in the carrier of (G.i); g +* (i,r) in the carrier of product G & g +* (i,s) in the carrier of product G by Th11,A3,A4,A5; then g +* (i,r) in product carr G & g +* (i,s) in product carr G by Th10; then A6: g +* (i,r) = g +* (i,s) by A2; i in dom G; then A7: i in dom g by A4,Lm1; then (g +* (i,r)).i = r by FUNCT_7:31; hence r=s by A6,A7,FUNCT_7:31; end; hence contradiction by ZFMISC_1:def 10; end; hence thesis by A1; end; end; theorem Th12: for G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G st p=p0 & q=q0 holds p+q = r0 iff for i be Element of dom G holds r0.i = p0.i + q0.i proof let G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G; assume A1: p=p0 & q=q0; len carr G = len G by PRVECT_2:def 4; then A2:dom carr G = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; A3: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hereby assume A4: p+q = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by A2; (addop G).i0 = the addF of (G.i0) by PRVECT_2:def 5; hence r0.i = p0.i + q0.i by A1,A4,A3,PRVECT_1:def 8; end; end; assume A5: for i be Element of dom G holds r0.i = p0.i + q0.i; reconsider pq=p+q as Element of product carr G by Th10; A6:ex g be Function st pq = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A7:ex g be Function st r0 = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be object; assume A8: i0 in dom pq; then reconsider i1=i0 as Element of dom G by A2,A6; reconsider i =i0 as Element of dom carr G by A8,A6; (addop G).i = the addF of (G.i) by PRVECT_2:def 5; then pq.i0 = p0.i1 + q0.i1 by A1,A3,PRVECT_1:def 8; hence pq.i0 = r0.i0 by A5; end; hence p+q = r0 by A6,A7,FUNCT_1:2; end; theorem Th13: for G be RealNormSpace-Sequence, p be Point of product G, r be Real, r0,p0 be Element of product carr G st p=p0 holds r*p = r0 iff for i be Element of dom G holds r0.i = r*(p0.i) proof let G be RealNormSpace-Sequence, p be Point of product G, r be Real, r0,p0 be Element of product carr G; assume A1: p=p0; hereby assume A2: r*p = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by Lm1; A3: (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8; reconsider rr=r as Element of REAL by XREAL_0:def 1; product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; hence r0.i = rr*(p0.i) by A1,A2,A3,PRVECT_2:def 2 .= r*(p0.i); end; end; assume A4: for i be Element of dom G holds r0.i = r* (p0.i); reconsider rp = r*p as Element of product carr G by Th10; A5:ex g be Function st rp = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A6:ex g be Function st r0 = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be object; assume A7: i0 in dom rp; then reconsider i1=i0 as Element of dom G by Lm1,A5; reconsider i=i0 as Element of dom carr G by A7,A5; A8: product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; reconsider r as Element of REAL by XREAL_0:def 1; (multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then rp.i0 = r*(p0.i1) by A1,A8,PRVECT_2:def 2; hence rp.i0 = r0.i0 by A4; end; hence r*p = r0 by A5,A6,FUNCT_1:2; end; theorem Th14: for G be RealNormSpace-Sequence, p0 be Element of product carr G holds 0.(product G)=p0 iff for i be Element of dom G holds p0.i = 0.(G.i) proof let G be RealNormSpace-Sequence, p0 be Element of product carr G; A1:dom carr G = dom G by Lm1; A2:product G = NORMSTR(# product carr G,zeros G,[:addop G:] ,[:multop G:], productnorm G #) by PRVECT_2:6; hence 0.(product G) = p0 implies for i be Element of dom G holds p0.i = 0.(G.i) by A1,PRVECT_2:def 7; assume A3:for i be Element of dom G holds p0.i = 0.(G.i); now let i0 be Element of dom carr G; reconsider i=i0 as Element of dom G by Lm1; p0.i0 = 0.(G.i) by A3; hence p0.i0 = the ZeroF of (G.i0); end; hence 0.(product G)=p0 by A2,PRVECT_2:def 7; end; theorem Th15: for G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G st p=p0 & q=q0 holds p-q = r0 iff for i be Element of dom G holds r0.i = p0.i - q0.i proof let G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G; assume A1: p=p0 & q=q0; reconsider qq0=(-1)*q as Element of product carr G by Th10; A2:p-q = p+(-1)*q by RLVECT_1:16; hereby assume A3: p-q = r0; thus for i be Element of dom G holds r0.i = p0.i - q0.i proof let i be Element of dom G; A4: r0.i = p0.i + qq0.i by Th12,A3,A1,A2; qq0.i = (-1)*(q0.i) by A1,Th13; hence thesis by A4,RLVECT_1:16; end; end; assume A5: for i be Element of dom G holds r0.i = p0.i - q0.i; now let i be Element of dom G; A6: qq0.i = (-1)*(q0.i) by A1,Th13; r0.i = p0.i - q0.i by A5; hence r0.i = p0.i + qq0.i by A6,RLVECT_1:16; end; hence p-q = r0 by A2,Th12,A1; end; begin :: Mean value theorem for vector-valued functions Lm2: now let S be RealLinearSpace; let p,q be Point of S; let z1 be Real; thus p+z1*(q-p) = p+(z1*q + (z1*(-p))) by RLVECT_1:def 5 .= p+(z1*q+- z1*p) by RLVECT_1:25 .= p+-z1*p+z1*q by RLVECT_1:def 3 .= 1*p-z1*p + z1*q by RLVECT_1:def 8 .= (1-z1)*p + z1*q by RLVECT_1:35; end; notation let S be RealLinearSpace; let p,q be Point of S; synonym [.p,q.] for LSeg(p,q); end; definition let S be RealLinearSpace; let p,q be Point of S; func ]. p,q .[ -> Subset of S equals [.p,q.] \ {p,q}; correctness; end; theorem LMOPN: for S be RealLinearSpace, p,q be Point of S st p <> q holds ].p,q.[ = { p+t*(q-p) where t is Real : 0 < t & t < 1} proof let S be RealLinearSpace, p,q be Point of S; assume AS1: p <> q; set A = { p+t*(q-p) where t is Real : 0 < t & t < 1}; for x be object holds (x in ].p,q.[ iff x in A) proof let x be object; hereby assume x in ].p,q.[; then P1: x in [.p,q.] & not x in {p,q} by XBOOLE_0:def 5; then x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1} by RLTOPSP1:def 2; then consider t be Real such that P2: x= (1-t)*p+t*q & 0 <= t & t <= 1; P3: x= p+t*(q-p) by P2,Lm2; P4: 0 <> t proof assume t = 0; then x = p + 0.S by P3,RLVECT_1:10 .= p by RLVECT_1:4; hence contradiction by P1,TARSKI:def 2; end; 1 <> t proof assume t = 1; then x = p + (q-p) by P3,RLVECT_1:def 8 .= q- (p - p) by RLVECT_1:29 .= q - 0.S by RLVECT_1:15 .= q by RLVECT_1:13; hence contradiction by P1,TARSKI:def 2; end; then 0 < t & t < 1 by P2,P4,XXREAL_0:1; hence x in A by P3; end; assume x in A; then consider t be Real such that P4: x= p+t*(q-p) & 0 < t & t < 1; x= (1-t)*p+t*q by Lm2,P4; then x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1} by P4; then P5: x in [.p,q.] by RLTOPSP1:def 2; P6: x <> p proof assume x = p; then P7: 0.S = t*(q-p) + p - p by P4,RLVECT_1:15 .= t*(q-p) + (p-p) by RLVECT_1:28 .= t*(q-p) + 0.S by RLVECT_1:15 .= t*(q-p) by RLVECT_1:4; q-p <> 0.S by AS1,RLVECT_1:21; hence contradiction by P4,P7,RLVECT_1:11; end; x <> q proof assume x = q; then q-p = t*(q-p) + (p-p) by P4,RLVECT_1:28 .=t*(q-p) + 0.S by RLVECT_1:15 .=t*(q-p) by RLVECT_1:4; then 1*(q-p) = t*(q-p) by RLVECT_1:def 8; then 1*(q-p) - t*(q-p) =0.S by RLVECT_1:15; then P7: (1-t)* (q-p) = 0.S by RLVECT_1:35; q-p <> 0.S by AS1,RLVECT_1:21; then 1-t = 0 by RLVECT_1:11,P7; hence contradiction by P4; end; then not x in {p,q} by P6,TARSKI:def 2; hence x in ]. p,q .[ by P5,XBOOLE_0:def 5; end; hence thesis by TARSKI:2; end; Lm3: for x be Real st for e be Real st 0 < e holds x <= e holds x <= 0 proof let x be Real; assume A1: for e be Real st 0 < e holds x <= e; assume A2: not x <= 0; then x <= x/2 by A1; then x - (x/2) <= (x/2) - (x/2) by XREAL_1:9; hence contradiction by A2; end; theorem Th17: for T be RealNormSpace, R be PartFunc of REAL,T st R is total holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.| ) < r proof let T be RealNormSpace, R be PartFunc of REAL,T; assume A1: R is total; A2:now assume A3: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.|) < r ); then consider r be Real such that A4: r > 0 and A5: for d be Real st d > 0 holds ex z be Real st z <> 0 & |.z.| < d & not ( ||. R/.z .||/ |.z.| ) < r; defpred P[Nat,Element of REAL] means $2 <> 0 & |.$2.| < (1/($1+1)) & not ( (||. R/.$2 .||/|.$2.| ) < r ); A6: now let n be Element of NAT; consider z be Real such that A7: z <> 0 & |.z.| < 1/(n + 1) & not ( ||. R/.z .||/ |.z.| ) < r by A5; reconsider z as Element of REAL by XREAL_0:def 1; take z; thus P[n,z] by A7; end; consider s be Real_Sequence such that A8: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6); A9: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A8; end; A10: now let p be Real; assume A11: 0

0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.| ) < r by A9,A16,A19; end; now assume A21: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.|) < r; now let s be 0-convergent non-zero Real_Sequence; A22: s is convergent & lim s = 0; A23: now let r be Real; assume r > 0; then consider d be Real such that A24: d > 0 and A25: for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.|) < r by A21; consider n be Nat such that A26: for m be Nat st n <=m holds |.s.m-0 .| < d by A22,A24,SEQ_2:def 7; take n; thus for m be Nat st n <=m holds ||. ((s")(#)(R/*s)).m- 0.T.|| < r proof dom R = REAL by A1,PARTFUN1:def 2; then A27: rng s c= dom R; let m be Nat; A28: m in NAT by ORDINAL1:def 12; assume n <=m; then A29: |.s.m-0 .| < d by A26; ||.(R/.(s.m)).|| / |.s.m.| = |.(s.m)".| * ||.(R/.(s.m)).|| by COMPLEX1:66 .= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1 .= ||.(s.m)"*((R/*s).m).|| by A27,FUNCT_2:109,A28 .= ||.(s".m)*((R/*s).m).|| by VALUED_1:10 .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2 .= ||. ((s")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13; hence thesis by A25,A29,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.T by A23,NORMSP_1:def 7; end; hence R is RestFunc-like by A1,NDIFF_3:def 1; end; hence thesis by A2; end; theorem Th18: for R be Function of REAL,REAL holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds (|.R.z.|/ |.z.|) < r proof let R be Function of REAL,REAL; A1:now assume A2: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( |.R.z.|/ |.z.| ) < r); then consider r be Real such that A3: r > 0 and A4: for d be Real st d > 0 holds ex z be Real st z <> 0 & |.z.| < d & not ( |.R.z.|/|.z.|) < r; defpred P[Nat,Element of REAL] means $2 <> 0 & |.$2.| < 1/($1+1) & not |.R.$2.|/|.$2.| < r; A5: now let n be Element of NAT; consider z be Real such that A6: z <> 0 & |.z.| < 1/(n + 1) & not ( |.R.z.|/|.z.|) < r by A4; reconsider z as Element of REAL by XREAL_0:def 1; take z; thus P[n,z] by A6; end; consider s be Real_Sequence such that A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A5); A8: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A7; end; A9: now let p be Real; assume A10: 0

0
ex d be Real st d > 0 & for z be Real st
z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r by A8,A15,A18;
end;
now assume
A19: for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r;
now let s be 0-convergent non-zero Real_Sequence;
A20: s is convergent & lim s = 0;
A21: now let r be Real;
assume A22: r > 0;
consider d be Real such that
A23: d > 0 and
A24: for z be Real st z <> 0 & |.z.| < d
holds |.R.z.|/|.z.| < r by A22,A19;
consider n be Nat such that
A25: for m be Nat st n <= m holds |.s.m-0 .| < d
by A20,A23,SEQ_2:def 7;
take n;
hereby let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume n <=m; then
A27: |.s.m-0 .| < d by A25;
|.R.(s.m).| / |.s.m.|
= |.(s.m)".| * |.R.(s.m).| by COMPLEX1:66
.= |.(s.m)" * R.(s.m).| by COMPLEX1:65
.= |.(s.m)" * (R/*s).m.| by FUNCT_2:115,A26
.= |.s".m * (R/*s).m .| by VALUED_1:10
.= |.(s"(#)(R/*s)).m - 0 .| by SEQ_1:8;
hence |. ((s")(#)(R/*s)).m- 0 .| < r by A24,A27,SEQ_1:5;
end;
end;
hence (s")(#)(R/*s) is convergent by SEQ_2:def 6;
hence lim((s")(#)(R/*s)) = 0 by A21,SEQ_2:def 7;
end;
hence R is RestFunc-like by FDIFF_1:def 2;
end;
hence thesis by A1;
end;
reconsider jj=1 as Real;
Lm4:
for T be RealNormSpace,
f be PartFunc of REAL,T,
g be PartFunc of REAL,REAL
st dom f = [.0,1.] & dom g = [.0,1.]
& f| [.0,1.] is continuous
& g| [.0,1.] is continuous
& f is_differentiable_on ].0,1.[
& g is_differentiable_on ].0,1.[
& (for x be Real st x in ].0,1.[ holds
||. diff(f,x) .|| <= diff(g,x))
holds
||. f/.1 -f/.0 .|| <= g/.1 - g/.0
proof
let T be RealNormSpace,
f be PartFunc of REAL,T,
g be PartFunc of REAL,REAL;
assume A1: dom f = [.0,1.] & dom g = [.0,1.]
& f| [.0,1.] is continuous
& g| [.0,1.] is continuous
& f is_differentiable_on ].0,1.[
& g is_differentiable_on ].0,1.[
& (for x be Real st x in ].0,1.[ holds
||. diff(f,x) .|| <= diff(g,x));
now let e be Real;
assume A2: 0 < e;
set e1=e/2;
set B = {x where x is Real : x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0};
now let z be object;
assume z in B; then
ex x be Real st z=x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
hence z in REAL;
end; then
reconsider B as Subset of REAL by TARSKI:def 3;
now let r be Real;
assume r in B; then
ex x be Real st r = x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then
A3: ex t be Real st r = t & 0<=t & t<=1; then
|.r.| = r by ABSVALUE:def 1;
hence |.r.| < 2 by A3,XXREAL_0:2;
end; then
A4: B is real-bounded by SEQ_4:4;
set s = upper_bound B;
A5: ex d be Real st 0 < d & d in B
proof
0 in [.0,1.]; then
consider d1 be Real such that
A6: 0 < d1 & for x1 be Real st x1 in [.0,1.] & |.x1-0 .| < d1
holds ||. f/.x1 - f/.0 .|| < e1 by A2,A1,NFCONT_3:17;
set d2=d1/2;
A7: d2 < d1 by A6,XREAL_1:216;
take d = min(d2,1);
thus A8: 0 < d by A6,XXREAL_0:21;
A9: d <= 1 by XXREAL_0:17; then
A10: d in [.0,1.] by A8;
A11: d <= d2 by XXREAL_0:17;
|.d-0 .| = d by A8,ABSVALUE:def 1; then
|.d-0 .| < d1 by A11,A7,XXREAL_0:2; then
A12: ||. f/.d - f/.0 .|| < e1 by A6,A10;
A13: [.0,d.] c= dom g by A1,A9,XXREAL_1:34;
A14: g| [.0,d.] is continuous by A1,A9,FCONT_1:16,XXREAL_1:34;
A15: ].0,d.[ c=].0,1.[ by A9,XXREAL_1:46; then
consider x0 be Real such that
A16: x0 in ].0,d.[
& diff(g,x0) =(g.d-g.0)/(d-0) by A1,A8,A13,A14,FDIFF_1:26,ROLLE:3;
||. diff(f,x0) .|| <= diff(g,x0) by A1,A16,A15; then
0 <= g.d-g.0 by A8,A16; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1
by A12,XREAL_1:7; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1+ e1*d
by A8,A2,XREAL_1:7; then
||. f/.d - f/.0 .|| -( (g.d - g.0) + e1+ e1*d ) <= 0 by XREAL_1:47; then
||. f/.d -f/.0 .|| - (g.d - g.0) - e1*d - e1 <= 0;
hence d in B by A10;
end; then
A17: 0 < s by A4,SEQ_4:def 1;
now let r be Real;
assume r in B; then
ex x be Real st r = x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0 ) - e1*x - e1 <= 0; then
ex t be Real st r=t & 0<=t & t<=1;
hence r<=1;
end; then
A18: s <= 1 by A5,SEQ_4:45;
defpred P[Nat,Element of REAL]
means $2 in B & |.s-$2.| <= 1/($1+1);
A19:now let x be Element of NAT;
reconsider t = 1/(1+x) as Real;
consider r be Real such that
A20: r in B & s-t < r by A4,A5,SEQ_4:def 1;
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
s-t + t < r + t by A20,XREAL_1:8; then
A21: s -r < t+r -r by XREAL_1:14;
r <= s by A4,A20,SEQ_4:def 1; then
0 <= s - r by XREAL_1:48;
hence P[x,r] by A20,A21,SEQ_2:1;
end;
consider sq be sequence of REAL such that
A22: for x being Element of NAT holds P[x, sq.x] from FUNCT_2:sch 3(A19);
A23: for x being Nat holds P[x, sq.x]
proof let x be Nat;
x in NAT by ORDINAL1:def 12;
hence thesis by A22;
end;
reconsider sq as Real_Sequence;
A24: now let p1 be Real;
assume A25: 0 < p1;
set p = p1/2;
consider n be Nat such that
A26: 1/p < n by SEQ_4:3;
1/p + (0 qua Real) < n+1 by A26,XREAL_1:8; then
A27: 1/(n+1) <= 1/(1/p) by A25,XREAL_1:118;
take n;
thus for m be Nat st n<=m holds |.sq.m-s.| < p1
proof
let m be Nat;
assume n<=m; then
0 < n+1 & n+1 <= m+1 by XREAL_1:6; then
1/(m+1) <= 1/(n+1) by XREAL_1:118; then
A28: 1/(m+1) <= p by A27,XXREAL_0:2;
sq.m in B & |.s-sq.m.| <= 1/(m+1) by A23; then
|.sq.m-s.| <= 1/(1+m) by COMPLEX1:60; then
A29: |.sq.m-s.| <= p by A28,XXREAL_0:2;
p < p1 by A25,XREAL_1:216;
hence thesis by A29,XXREAL_0:2;
end;
end; then
A30:sq is convergent by SEQ_2:def 6; then
A31:lim sq = s by A24,SEQ_2:def 7;
deffunc F(Real) = ||. f/.$1 -f/.0 .|| - (g.$1 - g.0) - e1*$1 - e1;
A32:for x being Element of REAL holds F(x) in REAL by XREAL_0:def 1;
consider Lg0 be Function of REAL,REAL such that
A33: for x being Element of REAL holds Lg0.x = F(x) from FUNCT_2:sch 8(A32);
A34: for x being Real holds Lg0.x = F(x)
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
Lg0.x = F(x) by A33;
hence thesis;
end;
set Lg = Lg0| [.0,1.];
A35: dom Lg0 = REAL by FUNCT_2:def 1; then
A36:
dom Lg = [.0,1.] by RELAT_1:62;
now let y be object;
assume y in rng sq; then
ex x be object st x in NAT & sq.x = y by FUNCT_2:11; then
y in B by A23; then
ex x be Real st y=x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
hence y in [.0,1.];
end; then
A37:
rng sq c= dom Lg by A36;
A38:s in [.0,1.] by A18,A17;
now let r be Real;
set r3=r/3;
assume A39: 0