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) st
( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent & f0 # x is subsequence of f # x )
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) st
( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent & f0 # x is subsequence of f # x )
let x be Point of X; :: thesis: ( ||.f.|| is bounded implies 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 ) )
assume ||.f.|| is bounded ; :: thesis: 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 )
then consider r0 being Real such that
B0: ( 0 < r0 & ( for m being Nat holds |.(||.f.|| . m).| < r0 ) ) by SEQ_2:3;
set r = (r0 * ||.x.||) + 1;
BS: for m being Nat holds |.((f # x) . m).| < (r0 * ||.x.||) + 1

proof

let m be Nat; :: thesis: |.((f # x) . m).| < (r0 * ||.x.||) + 1
reconsider h = f . m as Lipschitzian linear-Functional of X by DUALSP01:def 10;
|.(h . x).| = |.((f # x) . m).| by Def1;
then B5: |.((f # x) . m).| <= ||.(f . m).|| * ||.x.|| by DUALSP01:26;
( |.(||.f.|| . m).| <= r0 & ||.f.|| . m = ||.(f . m).|| ) by B0, NORMSP_0:def 4;
then ||.(f . m).|| <= r0 by ABSVALUE:def 1;
then ( ||.(f . m).|| * ||.x.|| <= r0 * ||.x.|| & r0 * ||.x.|| < (r0 * ||.x.||) + 1 ) by XREAL_1:29, XREAL_1:64;
then ||.(f . m).|| * ||.x.|| < (r0 * ||.x.||) + 1 by XXREAL_0:2;
hence |.((f # x) . m).| < (r0 * ||.x.||) + 1 by B5, XXREAL_0:2; :: thesis: verum

end;

reconsider seq = f # x as Real_Sequence ;
consider seq1 being Real_Sequence such that
X1: ( seq1 is subsequence of seq & seq1 is convergent ) by B0, SEQ_2:3, BS, SEQ_4:40;
consider N being increasing sequence of NAT such that
X2: seq1 = seq * N by X1, VALUED_0:def 17;
reconsider f0 = f * N as sequence of (DualSp X) ;

now :: thesis: for k being Nat holds (f0 # x) . k = seq1 . k

let k be Nat; :: thesis: (f0 # x) . k = seq1 . k
thus (f0 # x) . k = (f0 . k) . x by Def1
.= (f . (N . k)) . x by ORDINAL1:def 12, FUNCT_2:15
.= (f # x) . (N . k) by Def1
.= seq1 . k by X2, ORDINAL1:def 12, FUNCT_2:15 ; :: thesis: verum

end;

then X5: f0 # x = seq1 ;
for n being Nat holds |.(||.f0.|| . n).| < r0

proof

let n be Nat; :: thesis: |.(||.f0.|| . n).| < r0
||.f0.|| . n = ||.(f0 . n).|| by NORMSP_0:def 4;
then ||.f0.|| . n = ||.(f . (N . n)).|| by ORDINAL1:def 12, FUNCT_2:15;
then ||.f0.|| . n = ||.f.|| . (N . n) by NORMSP_0:def 4;
hence |.(||.f0.|| . n).| < r0 by B0; :: thesis: verum

end;

hence 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 ) by X1, X5, B0, SEQ_2:3; :: thesis: verum