let X be RealNormSpace; :: thesis: for g being sequence of (DualSp X) st g is convergent holds
( g is weakly*-convergent & w*-lim g = lim g )
let g be sequence of (DualSp X); :: thesis: ( g is convergent implies ( g is weakly*-convergent & w*-lim g = lim g ) )
assume A2: g is convergent ; :: thesis: ( g is weakly*-convergent & w*-lim g = lim g )
reconsider g0 = lim g as Point of (DualSp X) ;
A3: for x being Point of X holds
( g # x is convergent & lim (g # x) = g0 . x )

proof

let x be Point of X; :: thesis: ( g # x is convergent & lim (g # x) = g0 . x )
B2: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r )
set p = r / (||.x.|| + 1);
assume C00: 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r
then consider m being Nat such that
C1: for n being Nat st m <= n holds
||.((g . n) - g0).|| < r / (||.x.|| + 1) by A2, NORMSP_1:def 7;
(r / (||.x.|| + 1)) * (||.x.|| + 1) = r by XCMPLX_1:87;
then C0: ( 0 < r / (||.x.|| + 1) & (r / (||.x.|| + 1)) * ||.x.|| < r ) by C00, XREAL_1:29, XREAL_1:68;
CX: for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r

proof

let n be Nat; :: thesis: ( m <= n implies |.(((g # x) . n) - (g0 . x)).| < r )
assume m <= n ; :: thesis: |.(((g # x) . n) - (g0 . x)).| < r
then ||.((g . n) - g0).|| < r / (||.x.|| + 1) by C1;
then D4: ||.((g . n) - g0).|| * ||.x.|| <= (r / (||.x.|| + 1)) * ||.x.|| by XREAL_1:64;
D2: |.(((g # x) . n) - (g0 . x)).| = |.(((g . n) . x) - (g0 . x)).| by Def1
.= |.(((g . n) - g0) . x).| by DUALSP01:33 ;
reconsider h = (g . n) - g0 as Lipschitzian linear-Functional of X by DUALSP01:def 10;
|.(h . x).| <= ||.((g . n) - g0).|| * ||.x.|| by DUALSP01:26;
then |.(h . x).| <= (r / (||.x.|| + 1)) * ||.x.|| by D4, XXREAL_0:2;
hence |.(((g # x) . n) - (g0 . x)).| < r by D2, C0, XXREAL_0:2; :: thesis: verum

end;

take m ; :: thesis: for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r
thus for n being Nat st m <= n holds
|.(((g # x) . n) - (g0 . x)).| < r by CX; :: thesis: verum

end;

then g # x is convergent ;
hence ( g # x is convergent & lim (g # x) = g0 . x ) by B2, SEQ_2:def 7; :: thesis: verum

end;

then g is weakly*-convergent ;
hence ( g is weakly*-convergent & w*-lim g = lim g ) by A3, Def2; :: thesis: verum