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 )
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 )
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 ) )
assume AS0: ||.f.|| is bounded ; :: thesis: ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent )
consider r0 being Real such that
B0: ( 0 < r0 & ( for m being Nat holds |.(||.f.|| . m).| < r0 ) ) by AS0, SEQ_2:3;
set r = (r0 * ||.x.||) + 1;
C1: r0 * ||.x.|| < (r0 * ||.x.||) + 1 by XREAL_1:29;
BY: 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;
B5: |.(h . x).| <= ||.(f . m).|| * ||.x.|| by DUALSP01:26;
B3: |.(||.f.|| . m).| <= r0 by B0;
||.f.|| . m = ||.(f . m).|| by NORMSP_0:def 4;
then ||.(f . m).|| <= r0 by B3, ABSVALUE:def 1;
then C6: ||.(f . m).|| * ||.x.|| <= r0 * ||.x.|| by XREAL_1:64;
|.((f # x) . m).| = |.((f . m) . x).| by Def1;
then |.((f # x) . m).| <= r0 * ||.x.|| by B5, XXREAL_0:2, C6;
hence |.((f # x) . m).| < (r0 * ||.x.||) + 1 by C1, 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, BY, SEQ_4:40;
consider N being increasing sequence of NAT such that
X2: seq1 = seq * N by X1, VALUED_0:def 17;
set f0 = f * N;
for k being Nat holds ((f * N) # x) . k = seq1 . k

proof

let k be Nat; :: thesis: ((f * N) # x) . k = seq1 . k
thus ((f * N) # x) . k = ((f * N) . 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 Y5: (f * N) # x = seq1 ;
for n being Nat holds |.(||.(f * N).|| . n).| < r0

proof

let n be Nat; :: thesis: |.(||.(f * N).|| . n).| < r0
Y2: (f * N) . n = f . (N . n) by ORDINAL1:def 12, FUNCT_2:15;
||.(f * N).|| . n = ||.((f * N) . n).|| by NORMSP_0:def 4;
then ||.(f * N).|| . n = ||.f.|| . (N . n) by Y2, NORMSP_0:def 4;
hence |.(||.(f * N).|| . 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 ) by X1, Y5, B0, SEQ_2:3; :: thesis: verum