theorem Lm814: :: DUALSP03:25

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )