let X be RealNormSpace; :: thesis: for x being sequence of X st not X is trivial & x is weakly-convergent holds
( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )
let x be sequence of X; :: thesis: ( not X is trivial & x is weakly-convergent implies ( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) ) )
assume AS: ( not X is trivial & x is weakly-convergent ) ; :: thesis: ( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )
reconsider x0 = w-lim x as Point of X ;
for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for y being Point of X st y in rng x holds
|.(f . y).| <= Kf ) )

proof

let f be Point of (DualSp X); :: thesis: ex Kf being Real st
( 0 <= Kf & ( for y being Point of X st y in rng x holds
|.(f . y).| <= Kf ) )
reconsider h = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
h * x is convergent by AS;
then consider Kf being Real such that
A1: ( 0 < Kf & ( for n being Nat holds |.((h * x) . n).| < Kf ) ) by SEQ_2:3;
for y being Point of X st y in rng x holds
|.(f . y).| <= Kf

proof

let y be Point of X; :: thesis: ( y in rng x implies |.(f . y).| <= Kf )
assume y in rng x ; :: thesis: |.(f . y).| <= Kf
then consider m being Nat such that
A2: y = x . m by NFCONT_1:6;
|.((h * x) . m).| = |.(f . (x . m)).| by FUNCT_2:15, ORDINAL1:def 12;
hence |.(f . y).| <= Kf by A2, A1; :: thesis: verum

end;

hence ex Kf being Real st
( 0 <= Kf & ( for y being Point of X st y in rng x holds
|.(f . y).| <= Kf ) ) by A1; :: thesis: verum

end;

then consider K being Real such that
A4: ( 0 <= K & ( for y being Point of X st y in rng x holds
||.y.|| <= K ) ) by AS, DUALSP02:19;
A5: for n being Nat holds ||.x.|| . n <= K

proof

let n be Nat; :: thesis: ||.x.|| . n <= K
n in NAT by ORDINAL1:def 12;
then ||.(x . n).|| <= K by A4, FUNCT_2:4;
hence ||.x.|| . n <= K by NORMSP_0:def 4; :: thesis: verum

end;

A6: K + 0 < K + 1 by XREAL_1:8;
X10: for n being Nat holds |.(||.x.|| . n).| < K + 1

proof

let n be Nat; :: thesis: |.(||.x.|| . n).| < K + 1
||.x.|| . n <= K by A5;
then A7: ||.x.|| . n < K + 1 by A6, XXREAL_0:2;
0 <= ||.(x . n).|| ;
then 0 <= ||.x.|| . n by NORMSP_0:def 4;
hence |.(||.x.|| . n).| < K + 1 by A7, ABSVALUE:def 1; :: thesis: verum

end;

then X1: ||.x.|| is bounded by A4, SEQ_2:3;
B0: for f being Point of (DualSp X) holds |.(f . x0).| <= (lim_inf ||.x.||) * ||.f.||

proof

let f be Point of (DualSp X); :: thesis: |.(f . x0).| <= (lim_inf ||.x.||) * ||.f.||
reconsider h = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B1: ( h * x is convergent & lim (h * x) = h . x0 ) by DefWeaklim, AS;
B6: for n being Nat holds |.(h * x).| . n <= (||.f.|| (#) ||.x.||) . n

proof

let n be Nat; :: thesis: |.(h * x).| . n <= (||.f.|| (#) ||.x.||) . n
D21: |.(h . (x . n)).| <= ||.f.|| * ||.(x . n).|| by DUALSP01:26;
|.(h . (x . n)).| = |.((h * x) . n).| by FUNCT_2:15, ORDINAL1:def 12;
then |.((h * x) . n).| <= ||.f.|| * (||.x.|| . n) by D21, NORMSP_0:def 4;
then |.(h * x).| . n <= ||.f.|| * (||.x.|| . n) by SEQ_1:12;
hence |.(h * x).| . n <= (||.f.|| (#) ||.x.||) . n by SEQ_1:9; :: thesis: verum

end;

||.f.|| (#) ||.x.|| is bounded by A4, SEQ_2:3, X10, SEQM_3:37;
then lim_inf |.(h * x).| <= lim_inf (||.f.|| (#) ||.x.||) by B1, B6, RINFSUP1:91;
then B7: lim |.(h * x).| <= lim_inf (||.f.|| (#) ||.x.||) by B1, RINFSUP1:89;
lim_inf (||.f.|| (#) ||.x.||) = (lim_inf ||.x.||) * ||.f.|| by X1, LOPBAN_5:1;
hence |.(f . x0).| <= (lim_inf ||.x.||) * ||.f.|| by SEQ_4:14, B1, B7; :: thesis: verum

end;

now :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds 0 - s < ||.x.|| . (n + k)

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for k being Nat holds 0 - s < ||.x.|| . (n + k) )
assume D5: 0 < s ; :: thesis: ex n being Nat st
for k being Nat holds 0 - s < ||.x.|| . (n + k)
for k being Nat holds 0 - s < ||.x.|| . (0 + k)

proof

let k be Nat; :: thesis: 0 - s < ||.x.|| . (0 + k)
||.(x . k).|| = ||.x.|| . k by NORMSP_0:def 4;
hence 0 - s < ||.x.|| . (0 + k) by D5; :: thesis: verum

end;

hence ex n being Nat st
for k being Nat holds 0 - s < ||.x.|| . (n + k) ; :: thesis: verum

end;

then B8: 0 <= lim_inf ||.x.|| by X1, RINFSUP1:82;
consider Y being non empty Subset of REAL such that
B9: ( Y = { |.((Bound2Lipschitz (F,X)) . x0).| where F is Point of (DualSp X) : ||.F.|| <= 1 } & ||.x0.|| = upper_bound Y ) by AS, DUALSP02:7;

X21: now :: thesis: for r being Real st r in Y holds
r <= lim_inf ||.x.||

let r be Real; :: thesis: ( r in Y implies r <= lim_inf ||.x.|| )
assume r in Y ; :: thesis: r <= lim_inf ||.x.||
then consider F being Point of (DualSp X) such that
D7: ( r = |.((Bound2Lipschitz (F,X)) . x0).| & ||.F.|| <= 1 ) by B9;
reconsider f1 = F as Lipschitzian linear-Functional of X by DUALSP01:def 10;
D8: f1 = Bound2Lipschitz (F,X) by DUALSP01:23;
D9: |.(F . x0).| <= (lim_inf ||.x.||) * ||.F.|| by B0;
(lim_inf ||.x.||) * ||.F.|| <= (lim_inf ||.x.||) * 1 by B8, D7, XREAL_1:64;
hence r <= lim_inf ||.x.|| by D7, D8, D9, XXREAL_0:2; :: thesis: verum

end;

x0 in ClNLin (rng x)

proof

set M = ClNLin (rng x);
consider Z being Subset of X such that
C1: ( Z = the carrier of (Lin (rng x)) & ClNLin (rng x) = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by NORMSP_3:def 20;
reconsider Y = the carrier of (ClNLin (rng x)) as Subset of X by DUALSP01:def 16;
C3: Y is linearly-closed by NORMSP_3:29;
x0 in Y

proof

assume AS0: not x0 in Y ; :: thesis: contradiction
consider G being Point of (DualSp X) such that
C5: for y being Point of X st y in Y holds
(Bound2Lipschitz (G,X)) . y = 0 and
C6: (Bound2Lipschitz (G,X)) . x0 = 1 by C1, C3, AS0, DUALSP02:2;
reconsider g = G as Lipschitzian linear-Functional of X by DUALSP01:def 10;
C7: g = Bound2Lipschitz (G,X) by DUALSP01:23;
C8: g * x is convergent by AS;
C101: for n being Nat holds (g * x) . n <= (seq_const 0) . n

proof

let n be Nat; :: thesis: (g * x) . n <= (seq_const 0) . n
n in NAT by ORDINAL1:def 12;
then x . n in Lin (rng x) by RLVECT_3:15, FUNCT_2:4;
then x . n in Y by C1, NORMSP_3:4, TARSKI:def 3;
then g . (x . n) = 0 by C5, C7;
then (g * x) . n = 0 by FUNCT_2:15, ORDINAL1:def 12;
hence (g * x) . n <= (seq_const 0) . n ; :: thesis: verum

end;

C111: lim (seq_const 0) = (seq_const 0) . 0 by SEQ_4:26
.= 0 ;
lim (g * x) = g . x0 by DefWeaklim, AS
.= 1 by C6, DUALSP01:23 ;
hence contradiction by C111, C101, C8, SEQ_2:18; :: thesis: verum

end;

hence x0 in ClNLin (rng x) ; :: thesis: verum

end;

hence ( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) ) by A4, SEQ_2:3, X10, B9, SEQ_4:45, X21; :: thesis: verum