:: Uniform Boundedness Principle :: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama :: :: Received October 9, 2007 :: Copyright (c) 2007-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SEQ_1, REAL_1, XXREAL_2, CARD_1, XXREAL_0, ORDINAL2, VALUED_1, RELAT_1, RINFSUP1, FUNCT_2, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, ARYTM_3, COMPLEX1, NAT_1, SEQ_4, MEMBER_1, LOPBAN_1, NORMSP_2, REWRITE1, BHSP_3, RSSPACE3, METRIC_1, SEQ_2, NORMSP_1, PRE_TOPC, ARYTM_1, STRUCT_0, PROB_1, RCOMP_1, PCOMPS_1, NFCONT_1, CFCONT_1, FCONT_1, RLVECT_1, PARTFUN1, ZFMISC_1, CARD_3, SUPINF_2, PBOOLE, TOPS_1; notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, XCMPLX_0, PRE_TOPC, TOPS_1, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, CARD_3, NUMBERS, XREAL_0, RINFSUP1, XXREAL_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, XXREAL_2, RLVECT_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_0, NORMSP_1, NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2; constructors REAL_1, COMPLEX1, TOPS_1, TBSP_1, NFCONT_1, RINFSUP1, INTEGRA2, PROB_1, NORMSP_2, RSSPACE3, LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, PCOMPS_1, COMSEQ_2, BINOP_1; registrations NUMBERS, XREAL_0, XBOOLE_0, ORDINAL1, RELSET_1, STRUCT_0, MEMBERED, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1, VALUED_0, VALUED_1, SEQ_2, NORMSP_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, RSSPACE3, XXREAL_2; equalities RLVECT_1, METRIC_1, PCOMPS_1, NORMSP_2, RSSPACE3, LOPBAN_1, RINFSUP1, CARD_3, XCMPLX_0, NORMSP_0; expansions XXREAL_2; theorems TARSKI, XBOOLE_1, SEQ_1, SEQ_2, RLVECT_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_1, NORMSP_1, TBSP_1, PRE_TOPC, TOPS_1, NFCONT_1, XXREAL_0, FUNCT_1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, SEQM_3, INTEGRA2, SEQ_4, RSSPACE2, LOPBAN_1, LOPBAN_3, PROB_1, RSSPACE3, NAT_1, RELSET_1, VECTSP_1, NORMSP_0, XXREAL_2, ORDINAL1; schemes FUNCT_2, FRAENKEL; begin :: Uniform Boundedness Principle theorem Th1: for seq be Real_Sequence, r be Real st seq is bounded & 0<=r holds lim_inf(r(#)seq)=r*(lim_inf seq) proof let seq be Real_Sequence, r be Real; assume that A1: seq is bounded and A2: 0<=r; inferior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:8; then A3: ex f be Function st inferior_realsequence seq = f & dom f = NAT & rng f c= REAL by FUNCT_2:def 2; (inferior_realsequence seq).0 in rng inferior_realsequence seq by FUNCT_2:4; then reconsider X1 = rng inferior_realsequence seq as non empty Subset of REAL by A3; now let n be Element of NAT; consider r1 be Real such that A4: 0 complete; coherence proof now let S1 be sequence of MetricSpaceNorm X; reconsider S2=S1 as sequence of X; assume A1: S1 is Cauchy; S2 is Cauchy_sequence_by_Norm proof let r be Real; assume r > 0; then consider p be Nat such that A2: for n,m be Nat st p<=n & p<=m holds dist(S1.n,S1.m) < r by A1,TBSP_1:def 4; now let n,m be Nat; assume p<=n & p<=m; then dist(S1.n,S1.m) < r by A2; hence dist(S2.n,S2.m) < r by NORMSP_2:def 1; end; hence thesis; end; then S2 is convergent by LOPBAN_1:def 15; hence S1 is convergent by NORMSP_2:5; end; hence thesis by TBSP_1:def 5; end; end; definition let X be RealNormSpace, x0 be Point of X, r be Real; func Ball (x0,r) -> Subset of X equals { x where x is Point of X : ||.x0-x .|| < r }; coherence proof defpred P[Point of X] means ||.x0 - \$1.|| < r; {y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch 10; hence thesis; end; end; ::\$N Baire Category Theorem (Banach spaces) theorem Th3: :: Baire category theorem - Banach space version for X be RealBanachSpace, Y be SetSequence of X st union rng Y = the carrier of X & (for n be Nat holds Y.n is closed) ex n0 be Nat, r be Real, x0 be Point of X st 0 < r & Ball (x0,r) c= Y.n0 proof let X be RealBanachSpace, Y be SetSequence of X; assume that A1: union rng Y = the carrier of X and A2: for n be Nat holds Y.n is closed; now let n be Nat; reconsider Yn = Y.n as Subset of TopSpaceNorm X; Y.n is closed by A2; then Yn is closed by NORMSP_2:15; then Yn` is open by TOPS_1:3; hence (Y.n)` in Family_open_set MetricSpaceNorm X by PRE_TOPC:def 2; end; then consider n0 be Nat, r be Real, xx0 be Point of MetricSpaceNorm X such that A3: 0 < r & Ball(xx0,r) c= Y.n0 by A1,NORMSP_2:1; consider x0 be Point of X such that x0 = xx0 and A4: Ball(xx0,r) = {x where x is Point of X:||.x0-x.|| < r} by NORMSP_2:2; Ball (x0,r) = {x where x is Point of X : ||.x0-x.|| < r }; hence thesis by A3,A4; end; theorem Th4: for X,Y be RealNormSpace, f be Lipschitzian LinearOperator of X,Y holds f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & for x be Point of X holds f is_continuous_in x proof let X,Y be RealNormSpace, f be Lipschitzian LinearOperator of X,Y; consider K being Real such that A1: 0 <= K and A2: for x being VECTOR of X holds ||. f.x .|| <= K * ||. x .|| by LOPBAN_1:def 8; A3: now let x,y be Point of X; assume that x in the carrier of X and y in the carrier of X; f/.x -f/.y =f.x +(-1)* f.y by RLVECT_1:16; then f/.x -f/.y = f.x + f.((-1)*y) by LOPBAN_1:def 5; then f/.x -f/.y = f.(x+(-1)*y) by VECTSP_1:def 20; then A4: f/.x -f/.y =f.(x+-y) by RLVECT_1:16; ||.f/.x -f/.y .||<=K*||. x-y .||+||. x-y .|| by A2,A4,XREAL_1:38; hence ||. f/.x -f/.y .|| <= (K+1) * ||. x-y .||; end; dom f =the carrier of X by FUNCT_2:def 1; hence f is_Lipschitzian_on the carrier of X by A1,A3,NFCONT_1:def 9; hence A5: f is_continuous_on the carrier of X by NFCONT_1:45; hereby let x be Point of X; f|(the carrier of X) = f by RELSET_1:19; hence f is_continuous_in x by A5,NFCONT_1:def 7; end; end; theorem Th5: for X be RealBanachSpace, Y be RealNormSpace, T be Subset of R_NormSpace_of_BoundedLinearOperators(X,Y) st for x be Point of X ex K be Real st 0 <= K & for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||. f.x .|| <= K holds ex L be Real st 0 <= L & for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||.f.|| <= L proof let X be RealBanachSpace, Y be RealNormSpace, T be Subset of R_NormSpace_of_BoundedLinearOperators(X,Y); assume A1: for x be Point of X ex KTx be Real st 0 <= KTx & for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||. f.x .|| <= KTx; per cases; suppose A2: T <> {}; deffunc S0(Point of X,Real) = Ball(\$1,\$2); defpred P[Point of X,set] means \$2={||. f.\$1 .|| where f is Lipschitzian LinearOperator of X,Y :f in T}; A3: for x be Point of X ex y be Element of bool REAL st P[x,y] proof let x be Point of X; take y = {||. f.x .|| where f is Lipschitzian LinearOperator of X,Y : f in T}; now let z be object; assume z in y; then ex f be Lipschitzian LinearOperator of X,Y st z=||. f.x .|| & f in T; hence z in REAL; end; hence thesis by TARSKI:def 3; end; ex Ta be Function of the carrier of X,bool REAL st for x be Element of X holds P[x,Ta.x] from FUNCT_2:sch 3(A3); then consider Ta be Function of X,bool REAL such that A4: for x be Point of X holds Ta.x = {||. f.x .|| where f is Lipschitzian LinearOperator of X,Y :f in T}; defpred P[Nat,set] means \$2={x where x is Point of X: Ta.x is bounded_above & upper_bound(Ta.x) <= \$1}; A5: for n be Element of NAT ex y be Element of bool the carrier of X st P [n,y] proof let n be Element of NAT; take y = {x where x is Point of X: Ta.x is bounded_above & upper_bound(Ta.x) <= n}; now let z be object; assume z in y; then ex x be Point of X st z=x & Ta.x is bounded_above & upper_bound(Ta.x) <= n; hence z in the carrier of X; end; hence thesis by TARSKI:def 3; end; ex Xn be sequence of bool the carrier of X st for n be Element of NAT holds P[n,Xn.n] from FUNCT_2:sch 3(A5); then consider Xn be sequence of bool the carrier of X such that A6: for n be Element of NAT holds Xn.n = {x where x is Point of X: Ta .x is bounded_above & upper_bound(Ta.x) <= n}; reconsider Xn as SetSequence of X; A7: the carrier of X c= union rng Xn proof let x be object; assume x in the carrier of X; then reconsider x1=x as Point of X; consider KTx1 be Real such that 0 <= KTx1 and A8: for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||. f.x1 .|| <= KTx1 by A1; A9: Ta.x1 = {||. f.x1 .|| where f is Lipschitzian LinearOperator of X,Y :f in T} by A4; A10: for p be Real st p in Ta.x1 holds p <= KTx1 proof let p be Real; assume p in Ta.x1; then ex f be Lipschitzian LinearOperator of X,Y st p=||. f.x1 .|| & f in T by A9; hence thesis by A8; end; KTx1 is UpperBound of Ta.x1 proof let p be ExtReal; assume p in Ta.x1; then ex f be Lipschitzian LinearOperator of X,Y st p=||. f.x1 .|| & f in T by A9; hence thesis by A8; end; then A11: Ta.x1 is bounded_above; consider n be Nat such that A12: KTx1 0.X holds r/(2*||.x.||)*x+x0 in S0(x0,r) proof let x be Point of X; reconsider x1= (||.x.||")*x as Point of X; A46: ||.(r/2)*x1.|| = |.r/2.|*||.x1.|| by NORMSP_1:def 1; assume x <> 0.X; then A47: ||.x.|| <> 0 by NORMSP_0:def 5; ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x+(x0+-x0).|| by RLVECT_1:def 3; then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x+0.X.|| by RLVECT_1:5; then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x.|| by RLVECT_1:def 4; then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/2/(||.x.||)*x.|| by XCMPLX_1:78; then A48: ||. r/(2*||.x.||)*x+x0-x0.|| =||.(r/2)*x1.|| by RLVECT_1:def 7; A49: |. ||.x.||".| =||.x.||" by ABSVALUE:def 1; ||.x1.|| = |. ||.x.||".|*||.x.|| by NORMSP_1:def 1; then ||.x1.|| = 1 by A47,A49,XCMPLX_0:def 7; then ||.(r/2)*x1.|| = r/2 by A39,A46,ABSVALUE:def 1; then A50: ||.x0-(r/(2*||.x.||)*x+x0).|| =r/2 by A48,NORMSP_1:7; r/2 0.X holds ||.f.x.|| <= KT*||.x.|| proof A60: n0 in NAT by ORDINAL1:def 12; ||.x0-x0.||=||.0.X.|| by RLVECT_1:5; then x0 in S0(x0,r) by A39; then x0 in Xn.n0 by A40; then A61: x0 in {x1 where x1 is Point of X : Ta.x1 is bounded_above & upper_bound( Ta.x1) <= n0} by A6,A60; set nr3=||.f.x0.||; let x be Point of X; set nrp1=r/(2*||.x.||); set nrp2=(2*||.x.||)/r; set nr1=||.f.(r/(2*||.x.||)*x)+f.x0.||; set nr2=||.f.(r/(2*||.x.||)*x).||; ||.-(f.x0).||=||.f.x0.|| by NORMSP_1:2; then A62: nr2-nr3<=||.f.(r/(2*||.x.||)*x)-(-f.x0).|| by NORMSP_1:8; assume A63: x <> 0.X; then A64: ||. f.(r/(2*||.x.||)*x+x0) .|| <= n0 by A51,A45,A58; consider x1 be Point of X such that A65: x1=x0 and A66: Ta.x1 is bounded_above and upper_bound (Ta.x1) <= n0 by A61; Ta.x1 = {||. g.x1 .|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4; then ||. f.x0 .|| in Ta.x0 by A58,A65; then ||. f.x0 .|| <= upper_bound (Ta.x0) by A65,A66,SEQ_4:def 1; then A67: nrp1*||.f.x.|| - M <= nrp1*||.f.x.|| - nr3 by XREAL_1:10; ||.x.|| <> 0 by A63,NORMSP_0:def 5; then A68: ||.x.|| >0; ||. f.(r/(2*||.x.||)*x).|| =||.(r/(2*||.x.||))*f.x.|| by LOPBAN_1:def 5 ; then ||. f.(r/(2*||.x.||)*x).|| =|.r/(2*||.x.||).|*||.f.x.|| by NORMSP_1:def 1; then ||. f.(r/(2*||.x.||)*x).|| =(r/(2*||.x.||))*||.f.x.|| by A39, ABSVALUE:def 1; then ||.f.(r/(2*||.x.||)*x)+f.x0.|| =||.f.(r/(2*||.x.||)*x+x0).|| & ( r/(2*||.x.|| ))*||.f.x.||-nr3<=nr1 by A62,RLVECT_1:17,VECTSP_1:def 20; then (r/(2*||.x.||))*||.f.x.||-nr3<=n0 by A64,XXREAL_0:2; then nrp1*||.f.x.|| - M <= n0 by A67,XXREAL_0:2; then nrp1*||.f.x.|| + -M + M <= n0 + M by XREAL_1:6; then nrp2*(nrp1*||.f.x.||) <= nrp2*(n0+M) by A39,XREAL_1:64; then A69: nrp1*nrp2*||.f.x.|| <= nrp2*(n0+M); 2*||.x.|| >0 by A68,XREAL_1:129; then 1*||.f.x.|| <= nrp2*(n0+M) by A39,A69,XCMPLX_1:112; hence thesis; end; A70: for x be Point of X holds ||.f.x.|| <= KT*||.x.|| proof let x be Point of X; now assume A71: x = 0.X; then f.x = f.(0*0.X) by RLVECT_1:10; then f.x =0*f.(0.X) by LOPBAN_1:def 5; then A72: f.x =0.Y by RLVECT_1:10; ||.x.||= 0 by A71; hence thesis by A72; end; hence thesis by A59; end; thus for k be Real st k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT proof let k be Real; assume k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1}; then consider x be Point of X such that A73: k=||.f.x.|| & ||.x.|| <= 1; k <= KT*||.x.|| & KT*||.x.|| <=KT by A39,A44,A70,A73,XREAL_1:153; hence thesis by XXREAL_0:2; end; end; for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||.f.|| <= KT proof let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y); reconsider f1=f as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9; assume f in T; then A74: for k be Real st k in PreNorms(f1) holds k <= KT by A57; ||. f .|| = upper_bound PreNorms(f1) by LOPBAN_1:30; hence thesis by A74,SEQ_4:45; end; hence thesis by A39,A44; end; suppose A75: T = {}; take 0; thus thesis by A75; end; end; definition let X, Y be RealNormSpace, H be sequence of the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y), x be Point of X; func H # x -> sequence of Y means :Def2: for n be Nat holds it.n = (H.n).x; existence proof deffunc U(Nat) = (H.\$1).x; consider f being sequence of the carrier of Y such that A1: for n be Element of NAT holds f.n = U(n) from FUNCT_2:sch 4; take f; let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A1; end; uniqueness proof let S1,S2 be sequence of Y such that A2: for n be Nat holds S1.n = (H.n).x and A3: for n be Nat holds S2.n = (H.n).x; now let n be Element of NAT; S1.n = (H.n).x by A2; hence S1.n = S2.n by A3; end; hence thesis by FUNCT_2:63; end; end; theorem Th6: for X be RealBanachSpace, Y be RealNormSpace, vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y), tseq be Function of X,Y st ( for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x) ) holds tseq is Lipschitzian LinearOperator of X,Y & (for x be Point of X holds ||.tseq.x.|| <=(lim_inf ||.vseq.|| ) * ||.x.|| ) & for ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| proof let X be RealBanachSpace, Y be RealNormSpace, vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y), tseq be Function of X,Y; set T=rng vseq; set RNS=R_NormSpace_of_BoundedLinearOperators(X,Y); assume A1: for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x ); A2: for x,y be Point of X holds tseq.(x+y)= tseq.x + tseq.y proof let x,y be Point of X; A3: vseq#y is convergent & tseq.y = lim (vseq#y) by A1; A4: tseq.(x+y) = lim (vseq#(x+y)) by A1; now let n be Nat; vseq.n is Lipschitzian LinearOperator of X,Y & (vseq#(x+y)).n=(vseq.n).( x+y) by Def2,LOPBAN_1:def 9; then A5: (vseq#(x+y)).n=(vseq.n).x + (vseq.n).y by VECTSP_1:def 20; (vseq.n).y = (vseq#y).n by Def2; hence (vseq#(x+y)).n=(vseq#x).n + (vseq#y).n by A5,Def2; end; then A6: vseq#(x+y) = vseq#x + vseq#y by NORMSP_1:def 2; vseq#x is convergent & tseq.x = lim (vseq#x) by A1; hence thesis by A3,A6,A4,NORMSP_1:25; end; A7: for x be Point of X ex K be Real st 0 <= K & for f be Point of RNS st f in T holds ||. f.x .|| <= K proof let x be Point of X; vseq#x is convergent by A1; then ||. vseq#x .|| is bounded by NORMSP_1:23,SEQ_2:13; then consider K be Real such that A8: for n be Nat holds ||. vseq#x .||.n< K by SEQ_2:def 3; A9: for f be Point of RNS st f in T holds ||. f.x .|| <= K proof let f be Point of RNS; assume f in T; then consider n be object such that A10: n in NAT and A11: f=vseq.n by FUNCT_2:11; reconsider n as Nat by A10; (vseq.n).x = (vseq#x).n by Def2; then ||. f.x .|| = ||. vseq#x .||.n by A11,NORMSP_0:def 4; hence thesis by A8; end; ||. vseq#x .||.0< K by A8; then ||. (vseq#x).0 .|| < K by NORMSP_0:def 4; then 0 <= K; hence thesis by A9; end; vseq in Funcs(NAT,the carrier of RNS) by FUNCT_2:8; then ex f0 being Function st vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of RNS by FUNCT_2:def 2; then consider L be Real such that A12: 0 <= L and A13: for f be Point of RNS st f in T holds ||.f.|| <= L by A7,Th5; A14: L + 0 < 1+ L by XREAL_1:8; for n be Nat holds |.||.vseq.||.n .| < (1+L) proof let n be Nat; A15: n in NAT by ORDINAL1:def 12; ||.vseq.n.|| <= L by A13,FUNCT_2:4,A15; then ||.vseq.||.n <= L by NORMSP_0:def 4; then A16: ||.vseq.||.n <(1+L) by A14,XXREAL_0:2; 0<=||.vseq.n.||; then 0<=||.vseq.||.n by NORMSP_0:def 4; hence thesis by A16,ABSVALUE:def 1; end; then A17: ||.vseq.|| is bounded by A12,SEQ_2:3; A18: for x be Point of X holds ||.tseq.x.|| <=( lim_inf ||.vseq.|| ) * ||.x .|| proof let x be Point of X; A19: ||.x.|| (#) ||.vseq .|| is bounded by A17,SEQM_3:37; A20: for n be Nat holds ||.(vseq#x).n.|| <= ||.vseq.n.|| * ||.x .|| proof let n be Nat; (vseq.n).x = (vseq#x).n & vseq.n is Lipschitzian LinearOperator of X,Y by Def2,LOPBAN_1:def 9; hence thesis by LOPBAN_1:32; end; A21: for n be Nat holds ||. vseq#x .||.n <= (||.x.|| (#) ||. vseq .||).n proof let n be Nat; A22: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4; ||. vseq#x .||.n = ||.(vseq#x).n .|| & ||.(vseq#x).n .|| <= ||.vseq .n.|| * ||.x.|| by A20,NORMSP_0:def 4; hence thesis by A22,SEQ_1:9; end; A23: lim_inf (||.x.|| (#) ||.vseq .||) = ( lim_inf ||.vseq.|| ) * ||.x.|| by A17,Th1; A24: vseq#x is convergent & tseq.x = lim(vseq#x) by A1; then ||. vseq#x .|| is convergent by LOPBAN_1:20; then A25: lim ||. vseq#x .|| = lim_inf ||. vseq#x .|| by RINFSUP1:89; ||. vseq#x .|| is bounded by A24,LOPBAN_1:20,SEQ_2:13; then lim_inf ||. vseq#x .|| <=lim_inf (||.x.|| (#) ||.vseq .||) by A19,A21, RINFSUP1:91; hence thesis by A24,A23,A25,LOPBAN_1:20; end; now let s be Real; assume A26: 0 0 ex n0 be Nat st for n,m be Nat st n >= n0 & m >= n0 holds ||.(vseq#x).n -(vseq#x).m.||< TK1 proof let TK1 be Real such that A14: TK1 > 0; A15: 0= n0 & m >= n0 holds ||.((vseq #y).n) - ((vseq#y).m).|| < TK1/3 by A15,RSSPACE3:8; take n0; for n, m be Nat st n >= n0 & m >= n0 holds ||.(vseq#x).n -(vseq#x).m.||< TK1 proof let n,m be Nat; A21: m in NAT by ORDINAL1:def 12; A22: n in NAT by ORDINAL1:def 12; reconsider f = vseq.n as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9; reconsider g =vseq.m as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9; ||. (vseq#x).n - (vseq#y).m .|| <= ||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .|| by NORMSP_1:10; then A23: ||. (vseq#x).n - (vseq#y).m .|| + ||. (vseq#y).m - (vseq#x ).m .|| <= ||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .|| + ||. (vseq#y).m - (vseq#x).m .|| by XREAL_1:6; assume n >= n0 & m >= n0; then ||. (vseq#y).n - (vseq#y).m .|| < TK1/3 by A20; then ||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .|| < ||. (vseq#x).n - (vseq#y).n .||+ TK1/3 by XREAL_1:8; then A24: ||. (vseq#x).n - (vseq#y).n .||+ ||. (vseq#y).n - (vseq#y) .m .|| + ||. (vseq#y).m - (vseq#x).m .|| < ||. (vseq#x).n - (vseq#y).n .||+ TK1/3 + ||. (vseq#y).m - (vseq#x).m .|| by XREAL_1:8; ||. (vseq#x).m-(vseq#y).m .|| = ||. (vseq.m).x-(vseq#y).m .|| by Def2; then ||. (vseq#x).m-(vseq#y).m .|| = ||. g.x-g.y.|| by Def2; then A25: ||. (vseq#x).m-(vseq#y).m .|| <= M*||.x-y.|| by A11,FUNCT_2:4,A21; M*||.x-y.||