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))) ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
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))) ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
let x be sequence of X; :: thesis: ( ||.f.|| is bounded implies ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) ) )
assume ||.f.|| is bounded ; :: thesis: ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
then consider f0 being sequence of (DualSp X) such that
P0: ( f0 is subsequence of f & ||.f0.|| is bounded & f0 # (x . 0) is convergent & f0 # (x . 0) is subsequence of f # (x . 0) ) by Lm814A1;
consider N0 being V132() sequence of NAT such that
R0: f0 = f * N0 by VALUED_0:def 17, P0;
set D1 = Funcs (NAT, the carrier of (DualSp X));
set D2 = Funcs (NAT,NAT);
reconsider A = f0 as Element of Funcs (NAT, the carrier of (DualSp X)) by FUNCT_2:8;
reconsider B = N0 as Element of Funcs (NAT,NAT) by FUNCT_2:8;
defpred S1[ Nat, sequence of (DualSp X), sequence of NAT, sequence of (DualSp X), sequence of NAT] means ( ||.$2.|| is bounded implies ( $4 is subsequence of $2 & ||.$4.|| is bounded & $4 # (x . ($1 + 1)) is convergent & $4 # (x . ($1 + 1)) is subsequence of $2 # (x . ($1 + 1)) & $5 is V132() sequence of NAT & $4 = $2 * $5 ) );
P1: for n being Nat
for z being Element of Funcs (NAT, the carrier of (DualSp X))
for y being Element of Funcs (NAT,NAT) ex z1 being Element of Funcs (NAT, the carrier of (DualSp X)) ex y1 being Element of Funcs (NAT,NAT) st S1[n,z,y,z1,y1]
proof
let n be Nat; :: thesis: for z being Element of Funcs (NAT, the carrier of (DualSp X))
for y being Element of Funcs (NAT,NAT) ex z1 being Element of Funcs (NAT, the carrier of (DualSp X)) ex y1 being Element of Funcs (NAT,NAT) st S1[n,z,y,z1,y1]
let z be Element of Funcs (NAT, the carrier of (DualSp X)); :: thesis: for y being Element of Funcs (NAT,NAT) ex z1 being Element of Funcs (NAT, the carrier of (DualSp X)) ex y1 being Element of Funcs (NAT,NAT) st S1[n,z,y,z1,y1]
let y be Element of Funcs (NAT,NAT); :: thesis: ex z1 being Element of Funcs (NAT, the carrier of (DualSp X)) ex y1 being Element of Funcs (NAT,NAT) st S1[n,z,y,z1,y1]
consider f0 being sequence of (DualSp X), N being V132() sequence of NAT such that
X1: ( ||.z.|| is bounded implies ( f0 is subsequence of z & ||.f0.|| is bounded & f0 # (x . (n + 1)) is convergent & f0 # (x . (n + 1)) is subsequence of z # (x . (n + 1)) & f0 = z * N ) ) by Lm814A2;
reconsider z1 = f0 as Element of Funcs (NAT, the carrier of (DualSp X)) by FUNCT_2:8;
reconsider y1 = N as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take z1 ; :: thesis: ex y1 being Element of Funcs (NAT,NAT) st S1[n,z,y,z1,y1]
take y1 ; :: thesis: S1[n,z,y,z1,y1]
thus S1[n,z,y,z1,y1] by X1; :: thesis: verum
end;
consider F being sequence of (Funcs (NAT, the carrier of (DualSp X))), N being sequence of (Funcs (NAT,NAT)) such that
X2: ( F . 0 = A & N . 0 = B & ( for n being Nat holds S1[n,F . n,N . n,F . (n + 1),N . (n + 1)] ) ) from RECDEF_2:sch 3(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 & (F . ($1 + 1)) # (x . ($1 + 1)) is subsequence of (F . $1) # (x . ($1 + 1)) & N . ($1 + 1) is V132() sequence of NAT & F . ($1 + 1) = (F . $1) * (N . ($1 + 1)) );
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 ; :: thesis: ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
take N ; :: thesis: ( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )
thus ( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( 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 ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) ) by P0, X2, R0, Q2; :: thesis: verum