theorem :: DUALSP03:18

for X being RealBanachSpace
for f being sequence of (DualSp X) holds
( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 being Subset of X st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )