theorem Lm710A: :: DUALSP03:12

for X being RealNormSpace
for f being sequence of (DualSp X) st f is weakly-convergent holds
f is weakly*-convergent