theorem Th4: :: DUALSP07:4

for X being RealBanachSpace
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