let X be RealNormSpace; 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); 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; ( ||.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
; 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 S1[ 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 S1[n,z,y]
proof
let n be
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 S1[n,z,y]let z be
Element of
Funcs (
NAT, the
carrier of
(DualSp X));
ex y being Element of Funcs (NAT, the carrier of (DualSp X)) st S1[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
;
S1[n,z,y]
thus
S1[
n,
z,
y]
by X1;
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 S1[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(P1);
defpred S2[ Nat] means ( F . ($1 + 1) is subsequence of F . $1 & ||.(F . ($1 + 1)).|| is bounded & (F . ($1 + 1)) # (x . ($1 + 1)) is convergent );
Q0:
S2[ 0 ]
by X2, P0;
Q1:
for n being Nat st S2[n] holds
S2[n + 1]
by X2;
Q2:
for n being Nat holds S2[n]
from NAT_1:sch 2(Q0, Q1);
take
F
; ( 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; verum