let X be RealBanachSpace; :: thesis: for f being sequence of (DualSp X) st f is weakly*-convergent holds
( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| )
let f be sequence of (DualSp X); :: thesis: ( f is weakly*-convergent implies ( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| ) )
assume AS: f is weakly*-convergent ; :: thesis: ( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| )
reconsider f0 = w*-lim f as Point of (DualSp X) ;
for x being Point of X ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f holds
|.(g . x).| <= K ) )

proof

let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f holds
|.(g . x).| <= K ) )
f # x is convergent by AS;
then consider K being Real such that
A2: for n being Nat holds |.(f # x).| . n < K by SEQ_2:def 3;
A3: for g being Point of (DualSp X) st g in rng f holds
|.(g . x).| <= K

proof

let g be Point of (DualSp X); :: thesis: ( g in rng f implies |.(g . x).| <= K )
assume g in rng f ; :: thesis: |.(g . x).| <= K
then consider n being object such that
A4: ( n in NAT & g = f . n ) by FUNCT_2:11;
reconsider n = n as Nat by A4;
(f . n) . x = (f # x) . n by Def1;
then |.(g . x).| = |.(f # x).| . n by A4, SEQ_1:12;
hence |.(g . x).| <= K by A2; :: thesis: verum

end;

B6: |.(f # x).| . 0 < K by A2;
0 <= |.((f # x) . 0).| by COMPLEX1:46;
then 0 <= K by B6, SEQ_1:12;
hence ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f holds
|.(g . x).| <= K ) ) by A3; :: thesis: verum

end;

then consider L being Real such that
A7: 0 <= L and
A8: for g being Point of (DualSp X) st g in rng f holds
||.g.|| <= L by Lm55;
Y1: for n being Nat holds |.(||.f.|| . n).| < L + 1

proof

let n be Nat; :: thesis: |.(||.f.|| . n).| < L + 1
n in NAT by ORDINAL1:def 12;
then ||.(f . n).|| <= L by A8, FUNCT_2:4;
then ||.(f . n).|| < L + 1 by XREAL_1:39;
then |.||.(f . n).||.| < L + 1 by ABSVALUE:def 1;
hence |.(||.f.|| . n).| < L + 1 by NORMSP_0:def 4; :: thesis: verum

end;

then X1: ||.f.|| is bounded by A7, SEQ_2:3;
B1: for x being Point of X holds |.(f0 . x).| <= (lim_inf ||.f.||) * ||.x.||

proof

let x be Point of X; :: thesis: |.(f0 . x).| <= (lim_inf ||.f.||) * ||.x.||
B3: for n being Nat holds |.(f # x).| . n <= (||.x.|| (#) ||.f.||) . n

proof

let n be Nat; :: thesis: |.(f # x).| . n <= (||.x.|| (#) ||.f.||) . n
reconsider h = f . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B4: |.(f # x).| . n = |.((f # x) . n).| by SEQ_1:12;
||.(f . n).|| = ||.f.|| . n by NORMSP_0:def 4;
then ||.(f . n).|| * ||.x.|| = (||.x.|| (#) ||.f.||) . n by SEQ_1:9;
then |.(h . x).| <= (||.x.|| (#) ||.f.||) . n by DUALSP01:26;
hence |.(f # x).| . n <= (||.x.|| (#) ||.f.||) . n by B4, Def1; :: thesis: verum

end;

B6: lim_inf (||.x.|| (#) ||.f.||) = (lim_inf ||.f.||) * ||.x.|| by X1, LOPBAN_5:1;
B7: ( f # x is convergent & lim (f # x) = f0 . x ) by AS, Def2;
||.x.|| (#) ||.f.|| is bounded by A7, SEQ_2:3, Y1, SEQM_3:37;
then B9: lim_inf |.(f # x).| <= lim_inf (||.x.|| (#) ||.f.||) by B3, RINFSUP1:91, B7;
lim |.(f # x).| = |.(f0 . x).| by B7, SEQ_4:14;
hence |.(f0 . x).| <= (lim_inf ||.f.||) * ||.x.|| by B6, B7, RINFSUP1:89, B9; :: 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 < ||.f.|| . (n + k)

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

proof

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

end;

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

end;

then B10: 0 <= lim_inf ||.f.|| by X1, RINFSUP1:82;
reconsider g = f0 as Lipschitzian linear-Functional of X by DUALSP01:def 10;

now :: thesis: for k being Real st k in PreNorms g holds
k <= lim_inf ||.f.||

let k be Real; :: thesis: ( k in PreNorms g implies k <= lim_inf ||.f.|| )
assume k in PreNorms g ; :: thesis: k <= lim_inf ||.f.||
then consider x being Point of X such that
B11: ( k = |.(g . x).| & ||.x.|| <= 1 ) ;
B12: |.(f0 . x).| <= (lim_inf ||.f.||) * ||.x.|| by B1;
(lim_inf ||.f.||) * ||.x.|| <= (lim_inf ||.f.||) * 1 by B10, B11, XREAL_1:64;
hence k <= lim_inf ||.f.|| by B11, B12, XXREAL_0:2; :: thesis: verum

end;

then upper_bound (PreNorms g) <= lim_inf ||.f.|| by SEQ_4:45;
hence ( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| ) by A7, SEQ_2:3, Y1, DUALSP01:24; :: thesis: verum