theorem Lm814A1: :: DUALSP03:21

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