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

proof

let x be Point of X; :: thesis: ( f # x is convergent & lim (f # x) = f0 . x )
reconsider G = BiDual x as Lipschitzian linear-Functional of (DualSp X) by DUALSP01:def 10;
C3: ( G * f is convergent & lim (G * f) = G . f0 ) by DefWeaklim, AS;
B4: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r
then consider m being Nat such that
C1: for n being Nat st m <= n holds
|.(((G * f) . n) - (G . f0)).| < r by C3, SEQ_2:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r
thus for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r :: thesis: verum

proof

let n be Nat; :: thesis: ( m <= n implies |.(((f # x) . n) - (f0 . x)).| < r )
assume D3: m <= n ; :: thesis: |.(((f # x) . n) - (f0 . x)).| < r
B1: G . f0 = f0 . x by DUALSP02:def 1;
(G * f) . n = G . (f . n) by FUNCT_2:15, ORDINAL1:def 12
.= (f . n) . x by DUALSP02:def 1 ;
then (G * f) . n = (f # x) . n by Def1;
hence |.(((f # x) . n) - (f0 . x)).| < r by B1, C1, D3; :: thesis: verum

end;

end;

then f # x is convergent ;
hence ( f # x is convergent & lim (f # x) = f0 . x ) by B4, SEQ_2:def 7; :: thesis: verum

end;

hence f is weakly*-convergent ; :: thesis: verum