for X being RealBanachSpace
for f being sequence of (DualSp X) st X is separable & ||.f.|| is bounded holds
ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )