let X be RealBanachSpace; :: thesis: for X0, X1 being Subset of X
for vseq being sequence of (DualSp X) st X1 = the carrier of (Lin X0) & X1 is dense & ||.vseq.|| is bounded & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
vseq is weakly*-convergent
let X0, X1 be Subset of X; :: thesis: for vseq being sequence of (DualSp X) st X1 = the carrier of (Lin X0) & X1 is dense & ||.vseq.|| is bounded & ( 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: ( X1 = the carrier of (Lin X0) & X1 is dense & ||.vseq.|| is bounded & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) implies vseq is weakly*-convergent )
assume that
A1: X1 = the carrier of (Lin X0) and
A2: X1 is dense and
A3: ||.vseq.|| is bounded and
A4: for x being Point of X st x in X0 holds
vseq # x is convergent ; :: thesis: vseq is weakly*-convergent
for x being Point of X st x in X1 holds
vseq # x is convergent by STRUCT_0:def 5, Th3, A1, A4;
hence vseq is weakly*-convergent by A2, A3, DUALSP03:17; :: thesis: verum