let X be RealBanachSpace; :: thesis: for X0 being Subset of X
for vseq being sequence of (DualSp X) st ||.vseq.|| is bounded & X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
vseq is weakly*-convergent
let X0 be Subset of X; :: thesis: for vseq being sequence of (DualSp X) st ||.vseq.|| is bounded & X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
vseq is weakly*-convergent
let vseq be sequence of (DualSp X); :: thesis: ( ||.vseq.|| is bounded & X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) implies vseq is weakly*-convergent )
assume that
A1: ||.vseq.|| is bounded and
A2: X0 is dense and
A3: for x being Point of X st x in X0 holds
vseq # x is convergent ; :: thesis: vseq is weakly*-convergent
reconsider vseq1 = vseq as sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) by DUALSP02:14;
reconsider X01 = X0 as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
B1: for x being Point of X st x in X01 holds
vseq1 # x is convergent

proof

let x be Point of X; :: thesis: ( x in X01 implies vseq1 # x is convergent )
assume x in X01 ; :: thesis: vseq1 # x is convergent
then B11: vseq # x is convergent by A3;
vseq1 # x = vseq # x by RNSBH1;
hence vseq1 # x is convergent by RNS8, B11; :: thesis: verum

end;

B2: for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq1 # x) . n).|| <= K ) )

proof

let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq1 # x) . n).|| <= K ) )
consider K0 being Real such that
B20: ( 0 < K0 & ( for n being Nat holds |.(||.vseq.|| . n).| < K0 ) ) by A1, SEQ_2:3;
reconsider K = (K0 * ||.x.||) + 1 as Real ;
take K ; :: thesis: ( 0 <= K & ( for n being Nat holds ||.((vseq1 # x) . n).|| <= K ) )
C0: (K0 * ||.x.||) + 0 < (K0 * ||.x.||) + 1 by XREAL_1:8;
thus 0 <= K by B20; :: thesis: for n being Nat holds ||.((vseq1 # x) . n).|| <= K
thus for n being Nat holds ||.((vseq1 # x) . n).|| <= K :: thesis: verum

proof

let n be Nat; :: thesis: ||.((vseq1 # x) . n).|| <= K
|.(||.vseq.|| . n).| < K0 by B20;
then |.||.(vseq . n).||.| < K0 by NORMSP_0:def 4;
then A5: ||.(vseq . n).|| < K0 by ABSVALUE:def 1;
reconsider h = vseq . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B1: |.(h . x).| <= ||.(vseq . n).|| * ||.x.|| by DUALSP01:26;
C3: ||.(vseq . n).|| * ||.x.|| <= K0 * ||.x.|| by A5, XREAL_1:64;
|.((vseq # x) . n).| = |.((vseq . n) . x).| by Def1;
then |.((vseq # x) . n).| <= K0 * ||.x.|| by C3, B1, XXREAL_0:2;
then B4: |.((vseq # x) . n).| <= K by C0, XXREAL_0:2;
vseq # x = vseq1 # x by RNSBH1;
hence ||.((vseq1 # x) . n).|| <= K by B4, EUCLID:def 2; :: thesis: verum

end;

end;

X01 is dense by A2, NORMSP_3:15;
then consider tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) such that
B4: ( ( for x being Point of X holds
( vseq1 # x is convergent & tseq . x = lim (vseq1 # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq1.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq1.|| ) by B1, B2, LOPBAN_5:8;
reconsider g0 = tseq as Point of (DualSp X) by DUALSP02:14;
for x being Point of X holds
( vseq # x is convergent & lim (vseq # x) = g0 . x )

proof

let x be Point of X; :: thesis: ( vseq # x is convergent & lim (vseq # x) = g0 . x )
B7: vseq1 # x = vseq # x by RNSBH1;
( vseq1 # x is convergent & tseq . x = lim (vseq1 # x) ) by B4;
hence vseq # x is convergent by B7, RNS8; :: thesis: lim (vseq # x) = g0 . x
then lim (vseq # x) = lim (vseq1 # x) by RNSBH1, RNS9;
hence g0 . x = lim (vseq # x) by B4; :: thesis: verum

end;

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