let X be RealNormSpace; :: thesis: for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) )
let f be sequence of (DualSp X); :: thesis: for x being sequence of X st ||.f.|| is bounded holds
ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) )
let x be sequence of X; :: thesis: ( ||.f.|| is bounded implies ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) ) )
assume AS: ||.f.|| is bounded ; :: thesis: ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) )
set D = Funcs (NAT, the carrier of (DualSp X));
consider f0 being sequence of (DualSp X) such that
P0: ( f0 is subsequence of f & ||.f0.|| is bounded & f0 # (x . 0) is convergent ) by AS, Lm814A;
reconsider A = f0 as Element of Funcs (NAT, the carrier of (DualSp X)) by FUNCT_2:8;
defpred S₁[ Nat, sequence of (DualSp X), sequence of (DualSp X)] means ( ||.$2.|| is bounded implies ( $3 is subsequence of $2 & ||.$3.|| is bounded & $3 # (x . ($1 + 1)) is convergent ) );
P1: for n being Nat
for z being Element of Funcs (NAT, the carrier of (DualSp X)) ex y being Element of Funcs (NAT, the carrier of (DualSp X)) st S₁[n,z,y]

proof

let n be Nat; :: thesis: for z being Element of Funcs (NAT, the carrier of (DualSp X)) ex y being Element of Funcs (NAT, the carrier of (DualSp X)) st S₁[n,z,y]
let z be Element of Funcs (NAT, the carrier of (DualSp X)); :: thesis: ex y being Element of Funcs (NAT, the carrier of (DualSp X)) st S₁[n,z,y]
consider f0 being sequence of (DualSp X) such that
X1: ( ||.z.|| is bounded implies ( f0 is subsequence of z & ||.f0.|| is bounded & f0 # (x . (n + 1)) is convergent ) ) by Lm814A;
reconsider y = f0 as Element of Funcs (NAT, the carrier of (DualSp X)) by FUNCT_2:8;
take y ; :: thesis: S₁[n,z,y]
thus S₁[n,z,y] by X1; :: thesis: verum

end;

consider F being sequence of (Funcs (NAT, the carrier of (DualSp X))) such that
X2: ( F . 0 = A & ( for n being Nat holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(P1);
defpred S₂[ Nat] means ( F . ($1 + 1) is subsequence of F . $1 & ||.(F . ($1 + 1)).|| is bounded & (F . ($1 + 1)) # (x . ($1 + 1)) is convergent );
Q0: S₂[ 0 ] by X2, P0;
Q1: for n being Nat st S₂[n] holds
S₂[n + 1] by X2;
Q2: for n being Nat holds S₂[n] from NAT_1:sch 2(Q0, Q1);
take F ; :: thesis: ( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) )
thus ( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) ) by P0, X2, Q2; :: thesis: verum