theorem Lm814A2: :: DUALSP03:22

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) ex N being increasing sequence of NAT st
( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent & f0 # x is subsequence of f # x & f0 = f * N )