:: LOPBAN_5 semantic presentation begin theorem Th1: :: LOPBAN_5:1 for seq being Real_Sequence for r being Real st seq is bounded & 0 <= r holds lim_inf (r (#) seq) = r * (lim_inf seq) proof let seq be Real_Sequence; ::_thesis: for r being Real st seq is bounded & 0 <= r holds lim_inf (r (#) seq) = r * (lim_inf seq) let r be Real; ::_thesis: ( seq is bounded & 0 <= r implies lim_inf (r (#) seq) = r * (lim_inf seq) ) assume that A1: seq is bounded and A2: 0 <= r ; ::_thesis: lim_inf (r (#) seq) = r * (lim_inf seq) inferior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8; then A3: ex f being 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__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_(r_(#)_seq))_._n_=_(r_(#)_(inferior_realsequence_seq))_._n let n be Element of NAT ; ::_thesis: (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n consider r1 being real number such that A4: 0 < r1 and A5: for k being Element of NAT holds abs (seq . k) < r1 by A1, SEQ_2:3; seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:8; then ex f being Function st ( seq ^\ n = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2; then reconsider Y1 = rng (seq ^\ n) as non empty Subset of REAL by FUNCT_2:4; now__::_thesis:_for_k_being_Element_of_NAT_holds_abs_((seq_^\_n)_._k)_<_r1 let k be Element of NAT ; ::_thesis: abs ((seq ^\ n) . k) < r1 abs ((seq ^\ n) . k) = abs (seq . (n + k)) by NAT_1:def_3; hence abs ((seq ^\ n) . k) < r1 by A5; ::_thesis: verum end; then seq ^\ n is bounded by A4, SEQ_2:3; then A6: Y1 is bounded_below by RINFSUP1:6; (inferior_realsequence (r (#) seq)) . n = lower_bound ((r (#) seq) ^\ n) by RINFSUP1:36 .= lower_bound (r (#) (seq ^\ n)) by SEQM_3:21 .= lower_bound (r ** Y1) by INTEGRA2:17 .= r * (lower_bound (seq ^\ n)) by A2, A6, INTEGRA2:15 .= r * ((inferior_realsequence seq) . n) by RINFSUP1:36 ; hence (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n by SEQ_1:9; ::_thesis: verum end; then inferior_realsequence (r (#) seq) = r (#) (inferior_realsequence seq) by FUNCT_2:63; then A7: rng (inferior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17; inferior_realsequence seq is bounded by A1, RINFSUP1:56; then X1 is bounded_above by RINFSUP1:5; hence lim_inf (r (#) seq) = r * (lim_inf seq) by A2, A7, INTEGRA2:13; ::_thesis: verum end; theorem :: LOPBAN_5:2 for seq being Real_Sequence for r being Real st seq is bounded & 0 <= r holds lim_sup (r (#) seq) = r * (lim_sup seq) proof let seq be Real_Sequence; ::_thesis: for r being Real st seq is bounded & 0 <= r holds lim_sup (r (#) seq) = r * (lim_sup seq) let r be Real; ::_thesis: ( seq is bounded & 0 <= r implies lim_sup (r (#) seq) = r * (lim_sup seq) ) assume that A1: seq is bounded and A2: 0 <= r ; ::_thesis: lim_sup (r (#) seq) = r * (lim_sup seq) superior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8; then A3: ex f being Function st ( superior_realsequence seq = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2; (superior_realsequence seq) . 0 in rng (superior_realsequence seq) by FUNCT_2:4; then reconsider X1 = rng (superior_realsequence seq) as non empty Subset of REAL by A3; now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_realsequence_(r_(#)_seq))_._n_=_(r_(#)_(superior_realsequence_seq))_._n let n be Element of NAT ; ::_thesis: (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n consider r1 being real number such that A4: 0 < r1 and A5: for k being Element of NAT holds abs (seq . k) < r1 by A1, SEQ_2:3; seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:8; then ex f being Function st ( seq ^\ n = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2; then reconsider Y1 = rng (seq ^\ n) as non empty Subset of REAL by FUNCT_2:4; now__::_thesis:_for_k_being_Element_of_NAT_holds_abs_((seq_^\_n)_._k)_<_r1 let k be Element of NAT ; ::_thesis: abs ((seq ^\ n) . k) < r1 abs ((seq ^\ n) . k) = abs (seq . (n + k)) by NAT_1:def_3; hence abs ((seq ^\ n) . k) < r1 by A5; ::_thesis: verum end; then seq ^\ n is bounded by A4, SEQ_2:3; then A6: Y1 is bounded_above by RINFSUP1:5; (superior_realsequence (r (#) seq)) . n = upper_bound ((r (#) seq) ^\ n) by RINFSUP1:37 .= upper_bound (r (#) (seq ^\ n)) by SEQM_3:21 .= upper_bound (r ** Y1) by INTEGRA2:17 .= r * (upper_bound (seq ^\ n)) by A2, A6, INTEGRA2:13 .= r * ((superior_realsequence seq) . n) by RINFSUP1:37 ; hence (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n by SEQ_1:9; ::_thesis: verum end; then superior_realsequence (r (#) seq) = r (#) (superior_realsequence seq) by FUNCT_2:63; then A7: rng (superior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17; superior_realsequence seq is bounded by A1, RINFSUP1:56; then X1 is bounded_below by RINFSUP1:6; hence lim_sup (r (#) seq) = r * (lim_sup seq) by A2, A7, INTEGRA2:15; ::_thesis: verum end; registration let X be RealBanachSpace; cluster MetricSpaceNorm X -> complete ; coherence MetricSpaceNorm X is complete proof now__::_thesis:_for_S1_being_sequence_of_(MetricSpaceNorm_X)_st_S1_is_Cauchy_holds_ S1_is_convergent let S1 be sequence of (MetricSpaceNorm X); ::_thesis: ( S1 is Cauchy implies S1 is convergent ) reconsider S2 = S1 as sequence of X ; assume A1: S1 is Cauchy ; ::_thesis: S1 is convergent S2 is Cauchy_sequence_by_Norm proof let r be Real; :: according to RSSPACE3:def_5 ::_thesis: ( r <= 0 or ex b1 being Element of NAT st for b2, b3 being Element of NAT holds ( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) ) ) assume r > 0 ; ::_thesis: ex b1 being Element of NAT st for b2, b3 being Element of NAT holds ( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) ) then consider p being Element of NAT such that A2: for n, m being Element of NAT st p <= n & p <= m holds dist ((S1 . n),(S1 . m)) < r by A1, TBSP_1:def_4; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_p_<=_n_&_p_<=_m_holds_ dist_((S2_._n),(S2_._m))_<_r let n, m be Element of NAT ; ::_thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r ) assume ( p <= n & p <= m ) ; ::_thesis: dist ((S2 . n),(S2 . m)) < r then dist ((S1 . n),(S1 . m)) < r by A2; hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def_1; ::_thesis: verum end; hence ex b1 being Element of NAT st for b2, b3 being Element of NAT holds ( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) ) ; ::_thesis: verum end; then S2 is convergent by LOPBAN_1:def_15; hence S1 is convergent by NORMSP_2:5; ::_thesis: verum end; hence MetricSpaceNorm X is complete by TBSP_1:def_5; ::_thesis: verum end; end; definition let X be RealNormSpace; let x0 be Point of X; let r be real number ; func Ball (x0,r) -> Subset of X equals :: LOPBAN_5:def 1 { x where x is Point of X : ||.(x0 - x).|| < r } ; coherence { x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X proof defpred S1[ Point of X] means ||.(x0 - \$1).|| < r; { y where y is Point of X : S1[y] } c= the carrier of X from FRAENKEL:sch_10(); hence { x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X ; ::_thesis: verum end; end; :: deftheorem defines Ball LOPBAN_5:def_1_:_ for X being RealNormSpace for x0 being Point of X for r being real number holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ; theorem Th3: :: LOPBAN_5:3 for X being RealBanachSpace for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) holds ex n0 being Element of NAT ex r being Real ex x0 being Point of X st ( 0 < r & Ball (x0,r) c= Y . n0 ) proof let X be RealBanachSpace; ::_thesis: for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) holds ex n0 being Element of NAT ex r being Real ex x0 being Point of X st ( 0 < r & Ball (x0,r) c= Y . n0 ) let Y be SetSequence of X; ::_thesis: ( union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) implies ex n0 being Element of NAT ex r being Real ex x0 being Point of X st ( 0 < r & Ball (x0,r) c= Y . n0 ) ) assume that A1: union (rng Y) = the carrier of X and A2: for n being Element of NAT holds Y . n is closed ; ::_thesis: ex n0 being Element of NAT ex r being Real ex x0 being Point of X st ( 0 < r & Ball (x0,r) c= Y . n0 ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Y_._n)_`_in_Family_open_set_(MetricSpaceNorm_X) let n be Element of NAT ; ::_thesis: (Y . n) ` in Family_open_set (MetricSpaceNorm X) 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; ::_thesis: verum end; then consider n0 being Element of NAT , r being Real, xx0 being Point of (MetricSpaceNorm X) such that A3: ( 0 < r & Ball (xx0,r) c= Y . n0 ) by A1, NORMSP_2:1; consider x0 being 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 ex n0 being Element of NAT ex r being Real ex x0 being Point of X st ( 0 < r & Ball (x0,r) c= Y . n0 ) by A3, A4; ::_thesis: verum end; theorem Th4: :: LOPBAN_5:4 for X, Y being RealNormSpace for f being Lipschitzian LinearOperator of X,Y holds ( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) ) proof let X, Y be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,Y holds ( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) ) let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) ) 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__::_thesis:_for_x,_y_being_Point_of_X_st_x_in_the_carrier_of_X_&_y_in_the_carrier_of_X_holds_ ||.((f_/._x)_-_(f_/._y)).||_<=_(K_+_1)_*_||.(x_-_y).|| let x, y be Point of X; ::_thesis: ( x in the carrier of X & y in the carrier of X implies ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ) assume that x in the carrier of X and y in the carrier of X ; ::_thesis: ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| (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).|| ; ::_thesis: verum 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; ::_thesis: ( f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) ) hence A5: f is_continuous_on the carrier of X by NFCONT_1:45; ::_thesis: for x being Point of X holds f is_continuous_in x hereby ::_thesis: verum let x be Point of X; ::_thesis: f is_continuous_in x f | the carrier of X = f by RELSET_1:19; hence f is_continuous_in x by A5, NFCONT_1:def_7; ::_thesis: verum end; end; theorem Th5: :: LOPBAN_5:5 for X being RealBanachSpace for Y being RealNormSpace for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) ) holds ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) proof let X be RealBanachSpace; ::_thesis: for Y being RealNormSpace for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) ) holds ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) let Y be RealNormSpace; ::_thesis: for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) ) holds ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) let T be Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( ( for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) ) implies ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) ) assume A1: for x being Point of X ex KTx being real number st ( 0 <= KTx & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= KTx ) ) ; ::_thesis: ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) percases ( T <> {} or T = {} ) ; supposeA2: T <> {} ; ::_thesis: ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) deffunc H1( Point of X, Real) -> Subset of X = Ball (\$1,\$2); defpred S1[ Point of X, set ] means \$2 = { ||.(f . \$1).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ; A3: for x being Point of X ex y being Element of bool REAL st S1[x,y] proof let x be Point of X; ::_thesis: ex y being Element of bool REAL st S1[x,y] take y = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ; ::_thesis: ( y is Element of bool REAL & S1[x,y] ) now__::_thesis:_for_z_being_set_st_z_in_y_holds_ z_in_REAL let z be set ; ::_thesis: ( z in y implies z in REAL ) assume z in y ; ::_thesis: z in REAL then ex f being Lipschitzian LinearOperator of X,Y st ( z = ||.(f . x).|| & f in T ) ; hence z in REAL ; ::_thesis: verum end; hence ( y is Element of bool REAL & S1[x,y] ) by TARSKI:def_3; ::_thesis: verum end; ex Ta being Function of the carrier of X,(bool REAL) st for x being Element of X holds S1[x,Ta . x] from FUNCT_2:sch_3(A3); then consider Ta being Function of X,(bool REAL) such that A4: for x being Point of X holds Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ; defpred S2[ Element of NAT , set ] means \$2 = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= \$1 ) } ; A5: for n being Element of NAT ex y being Element of bool the carrier of X st S2[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of bool the carrier of X st S2[n,y] take y = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } ; ::_thesis: ( y is Element of bool the carrier of X & S2[n,y] ) now__::_thesis:_for_z_being_set_st_z_in_y_holds_ z_in_the_carrier_of_X let z be set ; ::_thesis: ( z in y implies z in the carrier of X ) assume z in y ; ::_thesis: z in the carrier of X then ex x being Point of X st ( z = x & Ta . x is bounded_above & upper_bound (Ta . x) <= n ) ; hence z in the carrier of X ; ::_thesis: verum end; hence ( y is Element of bool the carrier of X & S2[n,y] ) by TARSKI:def_3; ::_thesis: verum end; ex Xn being Function of NAT,(bool the carrier of X) st for n being Element of NAT holds S2[n,Xn . n] from FUNCT_2:sch_3(A5); then consider Xn being Function of NAT,(bool the carrier of X) such that A6: for n being 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 = Xn as SetSequence of X ; A7: the carrier of X c= union (rng Xn) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of X or x in union (rng Xn) ) assume x in the carrier of X ; ::_thesis: x in union (rng Xn) then reconsider x1 = x as Point of X ; consider KTx1 being real number such that 0 <= KTx1 and A8: for f being 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 being real number st p in Ta . x1 holds p <= KTx1 proof let p be real number ; ::_thesis: ( p in Ta . x1 implies p <= KTx1 ) assume p in Ta . x1 ; ::_thesis: p <= KTx1 then ex f being Lipschitzian LinearOperator of X,Y st ( p = ||.(f . x1).|| & f in T ) by A9; hence p <= KTx1 by A8; ::_thesis: verum end; KTx1 is UpperBound of Ta . x1 proof let p be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not p in Ta . x1 or p <= KTx1 ) assume p in Ta . x1 ; ::_thesis: p <= KTx1 then ex f being Lipschitzian LinearOperator of X,Y st ( p = ||.(f . x1).|| & f in T ) by A9; hence p <= KTx1 by A8; ::_thesis: verum end; then A11: Ta . x1 is bounded_above by XXREAL_2:def_10; consider n being Element of NAT such that A12: KTx1 < n by SEQ_4:3; consider f being set such that A13: f in T by A2, XBOOLE_0:def_1; reconsider f = f as Lipschitzian LinearOperator of X,Y by A13, LOPBAN_1:def_9; ||.(f . x1).|| in Ta . x by A9, A13; then upper_bound (Ta . x1) <= KTx1 by A10, SEQ_4:45; then upper_bound (Ta . x1) <= n by A12, XXREAL_0:2; then x1 in { z1 where z1 is Point of X : ( Ta . z1 is bounded_above & upper_bound (Ta . z1) <= n ) } by A11; then x1 in Xn . n by A6; then x1 in Union Xn by PROB_1:12; hence x in union (rng Xn) ; ::_thesis: verum end; A14: for x being Point of X holds not Ta . x is empty proof let x be Point of X; ::_thesis: not Ta . x is empty consider f0 being set such that A15: f0 in T by A2, XBOOLE_0:def_1; reconsider f0 = f0 as Lipschitzian LinearOperator of X,Y by A15, LOPBAN_1:def_9; Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4; then ||.(f0 . x).|| in Ta . x by A15; hence not Ta . x is empty ; ::_thesis: verum end; A16: for n being Element of NAT holds Xn . n is closed proof let n be Element of NAT ; ::_thesis: Xn . n is closed for s1 being sequence of X st rng s1 c= Xn . n & s1 is convergent holds lim s1 in Xn . n proof let s1 be sequence of X; ::_thesis: ( rng s1 c= Xn . n & s1 is convergent implies lim s1 in Xn . n ) assume that A17: rng s1 c= Xn . n and A18: s1 is convergent ; ::_thesis: lim s1 in Xn . n A19: Ta . (lim s1) = { ||.(f . (lim s1)).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4; A20: for y being real number st y in Ta . (lim s1) holds y <= n proof let y be real number ; ::_thesis: ( y in Ta . (lim s1) implies y <= n ) assume y in Ta . (lim s1) ; ::_thesis: y <= n then consider f being Lipschitzian LinearOperator of X,Y such that A21: y = ||.(f . (lim s1)).|| and A22: f in T by A19; A23: f is_continuous_in lim s1 by Th4; A24: dom f = the carrier of X by FUNCT_2:def_1; then A25: rng s1 c= dom f by A17, XBOOLE_1:1; then A26: f /* s1 is convergent by A18, A23, NFCONT_1:def_5; for k being Element of NAT holds ||.(f /* s1).|| . k <= n proof let k be Element of NAT ; ::_thesis: ||.(f /* s1).|| . k <= n ||.(f /* s1).|| . k = ||.((f /* s1) . k).|| by NORMSP_0:def_4; then A27: ||.(f /* s1).|| . k = ||.(f /. (s1 . k)).|| by A17, A24, FUNCT_2:109, XBOOLE_1:1; dom s1 = NAT by FUNCT_2:def_1; then s1 . k in rng s1 by FUNCT_1:3; then s1 . k in Xn . n by A17; then s1 . k in { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } by A6; then consider x being Point of X such that A28: x = s1 . k and A29: Ta . x is bounded_above and A30: upper_bound (Ta . x) <= n ; Ta . x = { ||.(g . x).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4; then ||.(f . (s1 . k)).|| in Ta . (s1 . k) by A22, A28; then ||.(f . (s1 . k)).|| <= upper_bound (Ta . (s1 . k)) by A28, A29, SEQ_4:def_1; hence ||.(f /* s1).|| . k <= n by A27, A28, A30, XXREAL_0:2; ::_thesis: verum end; then A31: for i being Element of NAT st 0 <= i holds ||.(f /* s1).|| . i <= n ; f /. (lim s1) = lim (f /* s1) by A18, A23, A25, NFCONT_1:def_5; then lim ||.(f /* s1).|| = ||.(f /. (lim s1)).|| by A26, LOPBAN_1:20; hence y <= n by A21, A26, A31, NORMSP_1:23, RSSPACE2:5; ::_thesis: verum end; then for y being ext-real number st y in Ta . (lim s1) holds y <= n ; then A32: n is UpperBound of Ta . (lim s1) by XXREAL_2:def_1; not Ta . (lim s1) is empty by A14; then A33: upper_bound (Ta . (lim s1)) <= n by A20, SEQ_4:45; A34: Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } by A6; Ta . (lim s1) is bounded_above by A32, XXREAL_2:def_10; hence lim s1 in Xn . n by A33, A34; ::_thesis: verum end; hence Xn . n is closed by NFCONT_1:def_3; ::_thesis: verum end; consider f being set such that A35: f in T by A2, XBOOLE_0:def_1; reconsider f = f as Lipschitzian LinearOperator of X,Y by A35, LOPBAN_1:def_9; union (rng Xn) is Subset of X by PROB_1:11; then union (rng Xn) = the carrier of X by A7, XBOOLE_0:def_10; then consider n0 being Element of NAT , r being Real, x0 being Point of X such that A36: 0 < r and A37: H1(x0,r) c= Xn . n0 by A16, Th3; ||.(x0 - x0).|| = ||.(0. X).|| by RLVECT_1:5; then x0 in H1(x0,r) by A36; then x0 in Xn . n0 by A37; then x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6; then consider xx1 being Point of X such that A38: xx1 = x0 and A39: Ta . xx1 is bounded_above and upper_bound (Ta . xx1) <= n0 ; Ta . xx1 = { ||.(g . xx1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4; then ||.(f . x0).|| in Ta . x0 by A38, A35; then ||.(f . x0).|| <= upper_bound (Ta . x0) by A38, A39, SEQ_4:def_1; then A40: 0 <= upper_bound (Ta . x0) ; A41: for x being Point of X st x <> 0. X holds ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) proof let x be Point of X; ::_thesis: ( x <> 0. X implies ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) ) reconsider x1 = (||.x.|| ") * x as Point of X ; A42: ||.((r / 2) * x1).|| = (abs (r / 2)) * ||.x1.|| by NORMSP_1:def_1; assume x <> 0. X ; ::_thesis: ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) then A43: ||.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 A44: ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / 2) * x1).|| by RLVECT_1:def_7; A45: abs (||.x.|| ") = ||.x.|| " by ABSVALUE:def_1; ||.x1.|| = (abs (||.x.|| ")) * ||.x.|| by NORMSP_1:def_1; then ||.x1.|| = 1 by A43, A45, XCMPLX_0:def_7; then ||.((r / 2) * x1).|| = r / 2 by A36, A42, ABSVALUE:def_1; then A46: ||.(x0 - (((r / (2 * ||.x.||)) * x) + x0)).|| = r / 2 by A44, NORMSP_1:7; r / 2 < r by A36, XREAL_1:216; hence ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) by A46; ::_thesis: verum end; set M = upper_bound (Ta . x0); take KT = (2 * ((upper_bound (Ta . x0)) + n0)) / r; ::_thesis: ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= KT ) ) A47: for f being Lipschitzian LinearOperator of X,Y st f in T holds for x being Point of X st x in H1(x0,r) holds ||.(f . x).|| <= n0 proof let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f in T implies for x being Point of X st x in H1(x0,r) holds ||.(f . x).|| <= n0 ) assume A48: f in T ; ::_thesis: for x being Point of X st x in H1(x0,r) holds ||.(f . x).|| <= n0 let x be Point of X; ::_thesis: ( x in H1(x0,r) implies ||.(f . x).|| <= n0 ) assume x in H1(x0,r) ; ::_thesis: ||.(f . x).|| <= n0 then x in Xn . n0 by A37; then x in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6; then consider x1 being Point of X such that A49: x1 = x and A50: Ta . x1 is bounded_above and A51: upper_bound (Ta . x1) <= n0 ; Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4; then ||.(f . x).|| in Ta . x by A48, A49; then ||.(f . x).|| <= upper_bound (Ta . x) by A49, A50, SEQ_4:def_1; hence ||.(f . x).|| <= n0 by A49, A51, XXREAL_0:2; ::_thesis: verum end; A52: now__::_thesis:_for_f_being_Lipschitzian_LinearOperator_of_X,Y_st_f_in_T_holds_ for_k_being_real_number_st_k_in__{__||.(f_._x1).||_where_x1_is_Point_of_X_:_||.x1.||_<=_1__}__holds_ k_<=_KT let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f in T implies for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT ) assume A53: f in T ; ::_thesis: for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT A54: for x being Point of X st x <> 0. X holds ||.(f . x).|| <= KT * ||.x.|| proof ||.(x0 - x0).|| = ||.(0. X).|| by RLVECT_1:5; then x0 in H1(x0,r) by A36; then x0 in Xn . n0 by A37; then A55: x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6; set nr3 = ||.(f . x0).||; let x be Point of X; ::_thesis: ( x <> 0. X implies ||.(f . x).|| <= KT * ||.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 A56: ||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).|| by NORMSP_1:8; assume A57: x <> 0. X ; ::_thesis: ||.(f . x).|| <= KT * ||.x.|| then A58: ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0 by A47, A41, A53; consider x1 being Point of X such that A59: x1 = x0 and A60: Ta . x1 is bounded_above and upper_bound (Ta . x1) <= n0 by A55; Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4; then ||.(f . x0).|| in Ta . x0 by A53, A59; then ||.(f . x0).|| <= upper_bound (Ta . x0) by A59, A60, SEQ_4:def_1; then A61: ((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| by XREAL_1:10; ||.x.|| <> 0 by A57, NORMSP_0:def_5; then A62: ||.x.|| > 0 ; ||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).|| by LOPBAN_1:def_5; then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = (abs (r / (2 * ||.x.||))) * ||.(f . x).|| by NORMSP_1:def_1; then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).|| by A36, ABSVALUE:def_1; then ( ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| & ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| ) by A56, VECTSP_1:def_20, RLVECT_1:17; then ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0 by A58, XXREAL_0:2; then ((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0 by A61, XXREAL_0:2; then (((r / (2 * ||.x.||)) * ||.(f . x).||) + (- (upper_bound (Ta . x0)))) + (upper_bound (Ta . x0)) <= n0 + (upper_bound (Ta . x0)) by XREAL_1:6; then ((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) by A36, XREAL_1:64; then A63: ((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) ; 2 * ||.x.|| > 0 by A62, XREAL_1:129; then 1 * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) by A36, A63, XCMPLX_1:112; hence ||.(f . x).|| <= KT * ||.x.|| ; ::_thesis: verum end; A64: for x being Point of X holds ||.(f . x).|| <= KT * ||.x.|| proof let x be Point of X; ::_thesis: ||.(f . x).|| <= KT * ||.x.|| now__::_thesis:_(_x_=_0._X_implies_||.(f_._x).||_<=_KT_*_||.x.||_) assume A65: x = 0. X ; ::_thesis: ||.(f . x).|| <= KT * ||.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 A66: f . x = 0. Y by RLVECT_1:10; ||.x.|| = 0 by A65; hence ||.(f . x).|| <= KT * ||.x.|| by A66; ::_thesis: verum end; hence ||.(f . x).|| <= KT * ||.x.|| by A54; ::_thesis: verum end; thus for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT ::_thesis: verum proof let k be real number ; ::_thesis: ( k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } implies k <= KT ) assume k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; ::_thesis: k <= KT then consider x being Point of X such that A67: ( k = ||.(f . x).|| & ||.x.|| <= 1 ) ; ( k <= KT * ||.x.|| & KT * ||.x.|| <= KT ) by A36, A40, A64, A67, XREAL_1:153; hence k <= KT by XXREAL_0:2; ::_thesis: verum end; end; for f being 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)); ::_thesis: ( f in T implies ||.f.|| <= KT ) reconsider f1 = f as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def_9; assume f in T ; ::_thesis: ||.f.|| <= KT then A68: for k being real number st k in PreNorms f1 holds k <= KT by A52; ||.f.|| = upper_bound (PreNorms f1) by LOPBAN_1:30; hence ||.f.|| <= KT by A68, SEQ_4:45; ::_thesis: verum end; hence ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= KT ) ) by A36, A40; ::_thesis: verum end; supposeA69: T = {} ; ::_thesis: ex L being real number st ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L ) ) take 0 ; ::_thesis: ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= 0 ) ) thus ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= 0 ) ) by A69; ::_thesis: verum end; end; end; definition let X, Y be RealNormSpace; let H be Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)); let x be Point of X; funcH # x -> sequence of Y means :Def2: :: LOPBAN_5:def 2 for n being Element of NAT holds it . n = (H . n) . x; existence ex b1 being sequence of Y st for n being Element of NAT holds b1 . n = (H . n) . x proof deffunc H1( Element of NAT ) -> Element of the carrier of Y = (H . \$1) . x; thus ex f being Function of NAT, the carrier of Y st for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of Y st ( for n being Element of NAT holds b1 . n = (H . n) . x ) & ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds b1 = b2 proof let S1, S2 be sequence of Y; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (H . n) . x ) & ( for n being Element of NAT holds S2 . n = (H . n) . x ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (H . n) . x and A2: for n being Element of NAT holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2 now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (H . n) . x by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines # LOPBAN_5:def_2_:_ for X, Y being RealNormSpace for H being Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for x being Point of X for b5 being sequence of Y holds ( b5 = H # x iff for n being Element of NAT holds b5 . n = (H . n) . x ); theorem Th6: :: LOPBAN_5:6 for X being RealBanachSpace for Y being RealNormSpace for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for tseq being Function of X,Y st ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) proof let X be RealBanachSpace; ::_thesis: for Y being RealNormSpace for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for tseq being Function of X,Y st ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) let Y be RealNormSpace; ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) for tseq being Function of X,Y st ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for tseq being Function of X,Y st ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) let tseq be Function of X,Y; ::_thesis: ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) implies ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) ) set T = rng vseq; set RNS = R_NormSpace_of_BoundedLinearOperators (X,Y); assume A1: for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) ) ; ::_thesis: ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) A2: for x, y being Point of X holds tseq . (x + y) = (tseq . x) + (tseq . y) proof let x, y be Point of X; ::_thesis: tseq . (x + y) = (tseq . x) + (tseq . y) A3: ( vseq # y is convergent & tseq . y = lim (vseq # y) ) by A1; A4: tseq . (x + y) = lim (vseq # (x + y)) by A1; now__::_thesis:_for_n_being_Element_of_NAT_holds_(vseq_#_(x_+_y))_._n_=_((vseq_#_x)_._n)_+_((vseq_#_y)_._n) let n be Element of NAT ; ::_thesis: (vseq # (x + y)) . n = ((vseq # x) . n) + ((vseq # y) . n) ( 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; ::_thesis: verum 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 tseq . (x + y) = (tseq . x) + (tseq . y) by A3, A6, A4, NORMSP_1:25; ::_thesis: verum end; A7: for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds ||.(f . x).|| <= K ) ) proof let x be Point of X; ::_thesis: ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds ||.(f . x).|| <= K ) ) vseq # x is convergent by A1; then ||.(vseq # x).|| is bounded by NORMSP_1:23, SEQ_2:13; then consider K being real number such that A8: for n being Element of NAT holds ||.(vseq # x).|| . n < K by SEQ_2:def_3; A9: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds ||.(f . x).|| <= K proof let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f in rng vseq implies ||.(f . x).|| <= K ) assume f in rng vseq ; ::_thesis: ||.(f . x).|| <= K then consider n being set such that A10: n in NAT and A11: f = vseq . n by FUNCT_2:11; reconsider n = n as Element of NAT by A10; (vseq . n) . x = (vseq # x) . n by Def2; then ||.(f . x).|| = ||.(vseq # x).|| . n by A11, NORMSP_0:def_4; hence ||.(f . x).|| <= K by A8; ::_thesis: verum end; ||.(vseq # x).|| . 0 < K by A8; then ||.((vseq # x) . 0).|| < K by NORMSP_0:def_4; then 0 <= K ; hence ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds ||.(f . x).|| <= K ) ) by A9; ::_thesis: verum end; vseq in Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by FUNCT_2:8; then ex f0 being Function st ( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) by FUNCT_2:def_2; then consider L being real number such that A12: 0 <= L and A13: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds ||.f.|| <= L by A7, Th5; A14: L + 0 < 1 + L by XREAL_1:8; for n being Element of NAT holds abs (||.vseq.|| . n) < 1 + L proof let n be Element of NAT ; ::_thesis: abs (||.vseq.|| . n) < 1 + L ||.(vseq . n).|| <= L by A13, FUNCT_2:4; then ||.vseq.|| . n <= L by NORMSP_0:def_4; then A15: ||.vseq.|| . n < 1 + L by A14, XXREAL_0:2; 0 <= ||.(vseq . n).|| ; then 0 <= ||.vseq.|| . n by NORMSP_0:def_4; hence abs (||.vseq.|| . n) < 1 + L by A15, ABSVALUE:def_1; ::_thesis: verum end; then A16: ||.vseq.|| is bounded by A12, SEQ_2:3; A17: for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| proof let x be Point of X; ::_thesis: ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| A18: ||.x.|| (#) ||.vseq.|| is bounded by A16, SEQM_3:37; A19: for n being Element of NAT holds ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| proof let n be Element of NAT ; ::_thesis: ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| ( (vseq . n) . x = (vseq # x) . n & vseq . n is Lipschitzian LinearOperator of X,Y ) by Def2, LOPBAN_1:def_9; hence ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| by LOPBAN_1:32; ::_thesis: verum end; A20: for n being Element of NAT holds ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n proof let n be Element of NAT ; ::_thesis: ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n A21: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def_4; ( ||.(vseq # x).|| . n = ||.((vseq # x) . n).|| & ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| ) by A19, NORMSP_0:def_4; hence ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n by A21, SEQ_1:9; ::_thesis: verum end; A22: lim_inf (||.x.|| (#) ||.vseq.||) = (lim_inf ||.vseq.||) * ||.x.|| by A16, Th1; A23: ( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1; then ||.(vseq # x).|| is convergent by LOPBAN_1:20; then A24: lim ||.(vseq # x).|| = lim_inf ||.(vseq # x).|| by RINFSUP1:89; ||.(vseq # x).|| is bounded by A23, LOPBAN_1:20, SEQ_2:13; then lim_inf ||.(vseq # x).|| <= lim_inf (||.x.|| (#) ||.vseq.||) by A18, A20, RINFSUP1:91; hence ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| by A23, A22, A24, LOPBAN_1:20; ::_thesis: verum end; now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_n_being_Element_of_NAT_st_ for_k_being_Element_of_NAT_holds_0_-_s_<_||.vseq.||_._(n_+_k) let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) ) assume A25: 0 < s ; ::_thesis: ex n being Element of NAT st for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) for k being Element of NAT holds 0 - s < ||.vseq.|| . (0 + k) proof let k be Element of NAT ; ::_thesis: 0 - s < ||.vseq.|| . (0 + k) ||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def_4; then 0 <= ||.vseq.|| . k ; hence 0 - s < ||.vseq.|| . (0 + k) by A25; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) ; ::_thesis: verum end; then A26: 0 <= lim_inf ||.vseq.|| by A16, RINFSUP1:82; A27: for x being Point of X for r being Element of REAL holds tseq . (r * x) = r * (tseq . x) proof let x be Point of X; ::_thesis: for r being Element of REAL holds tseq . (r * x) = r * (tseq . x) let r be Element of REAL ; ::_thesis: tseq . (r * x) = r * (tseq . x) A28: tseq . x = lim (vseq # x) by A1; A29: now__::_thesis:_for_n_being_Element_of_NAT_holds_(vseq_#_(r_*_x))_._n_=_r_*_((vseq_#_x)_._n) let n be Element of NAT ; ::_thesis: (vseq # (r * x)) . n = r * ((vseq # x) . n) ( vseq . n is Lipschitzian LinearOperator of X,Y & (vseq # (r * x)) . n = (vseq . n) . (r * x) ) by Def2, LOPBAN_1:def_9; then (vseq # (r * x)) . n = r * ((vseq . n) . x) by LOPBAN_1:def_5; hence (vseq # (r * x)) . n = r * ((vseq # x) . n) by Def2; ::_thesis: verum end; tseq . (r * x) = lim (vseq # (r * x)) by A1; then tseq . (r * x) = lim (r * (vseq # x)) by A29, NORMSP_1:def_5; hence tseq . (r * x) = r * (tseq . x) by A1, A28, NORMSP_1:28; ::_thesis: verum end; then reconsider tseq1 = tseq as Lipschitzian LinearOperator of X,Y by A2, A17, A26, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8; for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| proof for k being real number st k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= lim_inf ||.vseq.|| proof let k be real number ; ::_thesis: ( k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } implies k <= lim_inf ||.vseq.|| ) assume k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; ::_thesis: k <= lim_inf ||.vseq.|| then consider x being Point of X such that A30: ( k = ||.(tseq . x).|| & ||.x.|| <= 1 ) ; ( k <= (lim_inf ||.vseq.||) * ||.x.|| & (lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.|| ) by A17, A26, A30, XREAL_1:153; hence k <= lim_inf ||.vseq.|| by XXREAL_0:2; ::_thesis: verum end; then A31: upper_bound (PreNorms tseq1) <= lim_inf ||.vseq.|| by SEQ_4:45; let ttseq be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( ttseq = tseq implies ||.ttseq.|| <= lim_inf ||.vseq.|| ) assume ttseq = tseq ; ::_thesis: ||.ttseq.|| <= lim_inf ||.vseq.|| hence ||.ttseq.|| <= lim_inf ||.vseq.|| by A31, LOPBAN_1:30; ::_thesis: verum end; hence ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.|| ) ) by A2, A27, A17, A26, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8; ::_thesis: verum end; begin theorem Th7: :: LOPBAN_5:7 for X being RealBanachSpace for X0 being Subset of (LinearTopSpaceNorm X) for Y being RealBanachSpace for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds for x being Point of X holds vseq # x is convergent proof let X be RealBanachSpace; ::_thesis: for X0 being Subset of (LinearTopSpaceNorm X) for Y being RealBanachSpace for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds for x being Point of X holds vseq # x is convergent let X0 be Subset of (LinearTopSpaceNorm X); ::_thesis: for Y being RealBanachSpace for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds for x being Point of X holds vseq # x is convergent let Y be RealBanachSpace; ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds for x being Point of X holds vseq # x is convergent let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) implies for x being Point of X holds vseq # x is convergent ) assume A1: X0 is dense ; ::_thesis: ( ex x being Point of X st ( x in X0 & not vseq # x is convergent ) or ex x being Point of X st for K being real number holds ( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent ) set T = rng vseq; assume A2: for x being Point of X st x in X0 holds vseq # x is convergent ; ::_thesis: ( ex x being Point of X st for K being real number holds ( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent ) vseq in Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by FUNCT_2:8; then ex f0 being Function st ( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) by FUNCT_2:def_2; then reconsider T = rng vseq as Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; assume A3: for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ; ::_thesis: for x being Point of X holds vseq # x is convergent for x being Point of X ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) proof let x be Point of X; ::_thesis: ex K being real number st ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) consider K being real number such that A4: 0 <= K and A5: for n being Element of NAT holds ||.((vseq # x) . n).|| <= K by A3; take K ; ::_thesis: ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) now__::_thesis:_for_f_being_Point_of_(R_NormSpace_of_BoundedLinearOperators_(X,Y))_st_f_in_T_holds_ ||.(f_._x).||_<=_K let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f in T implies ||.(f . x).|| <= K ) assume f in T ; ::_thesis: ||.(f . x).|| <= K then consider n being set such that A6: n in NAT and A7: f = vseq . n by FUNCT_2:11; reconsider n = n as Element of NAT by A6; ||.(f . x).|| = ||.((vseq # x) . n).|| by A7, Def2; hence ||.(f . x).|| <= K by A5; ::_thesis: verum end; hence ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K ) ) by A4; ::_thesis: verum end; then consider L being real number such that A8: 0 <= L and A9: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L by Th5; set M = 1 + L; A10: L + 0 < 1 + L by XREAL_1:8; A11: for f being Lipschitzian LinearOperator of X,Y st f in T holds for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| proof let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f in T implies for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| ) reconsider f1 = f as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9; assume f in T ; ::_thesis: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| then ||.f1.|| <= L by A9; then A12: ||.f1.|| < 1 + L by A10, XXREAL_0:2; let x, y be Point of X; ::_thesis: ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| ||.((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 A13: ||.((f . x) - (f . y)).|| = ||.(f . (x - y)).|| by RLVECT_1:16; ( ||.(f . (x - y)).|| <= ||.f1.|| * ||.(x - y).|| & ||.f1.|| * ||.(x - y).|| <= (1 + L) * ||.(x - y).|| ) by A12, LOPBAN_1:32, XREAL_1:64; hence ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| by A13, XXREAL_0:2; ::_thesis: verum end; hereby ::_thesis: verum let x be Point of X; ::_thesis: vseq # x is convergent for TK1 being Real st TK1 > 0 holds ex n0 being Element of NAT st for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 proof let TK1 be Real; ::_thesis: ( TK1 > 0 implies ex n0 being Element of NAT st for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 ) assume A14: TK1 > 0 ; ::_thesis: ex n0 being Element of NAT st for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 A15: 0 < TK1 / 3 by A14, XREAL_1:222; set V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ; { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } c= the carrier of X proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } or s in the carrier of X ) assume s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ; ::_thesis: s in the carrier of X then ex z being Point of X st ( s = z & ||.(x - z).|| < TK1 / (3 * (1 + L)) ) ; hence s in the carrier of X ; ::_thesis: verum end; then reconsider V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def_4; 0 < 3 * (1 + L) by A8, XREAL_1:129; then 0 < TK1 / (3 * (1 + L)) by A14, XREAL_1:139; then ||.(x - x).|| < TK1 / (3 * (1 + L)) by NORMSP_1:6; then ( V is open & x in V ) by NORMSP_2:23; then X0 meets V by A1, TOPS_1:45; then consider s being set such that A16: s in X0 and A17: s in V by XBOOLE_0:3; consider y being Point of X such that A18: s = y and A19: ||.(x - y).|| < TK1 / (3 * (1 + L)) by A17; for s being Real st 0 < s holds ex n1 being Element of NAT st for m1 being Element of NAT st n1 <= m1 holds ||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s by A2, A16, A18, LOPBAN_3:4; then vseq # y is Cauchy_sequence_by_Norm by LOPBAN_3:5; then consider n0 being Element of NAT such that A20: for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A15, RSSPACE3:8; take n0 ; ::_thesis: for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 proof let n, m be Element of NAT ; ::_thesis: ( n >= n0 & m >= n0 implies ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 ) 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 A21: ||.(((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 ) ; ::_thesis: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 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 A22: (||.(((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 A23: ||.(((vseq # x) . m) - ((vseq # y) . m)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4; (1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68; then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92; then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| < TK1 / 3 by A23, XXREAL_0:2; then ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < TK1 / 3 by NORMSP_1:7; then A24: ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by XREAL_1:8; ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.(((vseq . n) . x) - ((vseq # y) . n)).|| by Def2; then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.((f . x) - (f . y)).|| by Def2; then A25: ||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4; ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by NORMSP_1:10; then ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A21, XXREAL_0:2; then A26: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A22, XXREAL_0:2; (1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68; then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92; then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| < TK1 / 3 by A25, XXREAL_0:2; then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) < (TK1 / 3) + (TK1 / 3) by XREAL_1:8; then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:8; then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by A24, XXREAL_0:2; hence ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 by A26, XXREAL_0:2; ::_thesis: verum end; hence for n, m being Element of NAT st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 ; ::_thesis: verum end; then vseq # x is Cauchy_sequence_by_Norm by RSSPACE3:8; hence vseq # x is convergent by LOPBAN_1:def_15; ::_thesis: verum end; end; theorem :: LOPBAN_5:8 for X, Y being RealBanachSpace for X0 being Subset of (LinearTopSpaceNorm X) for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) proof let X, Y be RealBanachSpace; ::_thesis: for X0 being Subset of (LinearTopSpaceNorm X) for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) let X0 be Subset of (LinearTopSpaceNorm X); ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds vseq # x is convergent ) & ( for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) implies ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) ) assume A1: X0 is dense ; ::_thesis: ( ex x being Point of X st ( x in X0 & not vseq # x is convergent ) or ex x being Point of X st for K being real number holds ( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) ) deffunc H1( Point of X) -> Element of the carrier of Y = lim (vseq # \$1); assume A2: for x being Point of X st x in X0 holds vseq # x is convergent ; ::_thesis: ( ex x being Point of X st for K being real number holds ( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) ) consider tseq being Function of X,Y such that A3: for x being Point of X holds tseq . x = H1(x) from FUNCT_2:sch_4(); assume for x being Point of X ex K being real number st ( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ; ::_thesis: ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) then A4: for x being Point of X holds vseq # x is convergent by A1, A2, Th7; then reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A3, Th6; reconsider tseq = tseq as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9; take tseq ; ::_thesis: ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) thus ( ( for x being Point of X holds ( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) by A4, A3, Th6; ::_thesis: verum end;