let X be RealNormSpace; :: thesis: 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 )
let f be sequence of (DualSp X); :: thesis: 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 )
let x be Point of X; :: thesis: ( ||.f.|| is bounded implies 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 ) )
assume ||.f.|| is bounded ; :: thesis: 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 )
then consider f0 being sequence of (DualSp X) such that
A1: ( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent & f0 # x is subsequence of f # x ) by Lm814A1;
take f0 ; :: thesis: 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 )
ex N being increasing sequence of NAT st f0 = f * N by A1, VALUED_0:def 17;
hence 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 ) by A1; :: thesis: verum