let X be RealNormSpace; :: thesis: for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
let f be sequence of (DualSp X); :: thesis: for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
let x be sequence of X; :: thesis: ( ||.f.|| is bounded implies ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) ) )
assume ||.f.|| is bounded ; :: thesis: ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )
then consider F being sequence of (Funcs (NAT, the carrier of (DualSp X))), N being sequence of (Funcs (NAT,NAT)) such that
A0: ( 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 Lm814C;
deffunc H1( Element of NAT ) -> Element of the carrier of (DualSp X) = (F . $1) . $1;
consider M being Function of NAT,(DualSp X) such that
A1: for k being Element of NAT holds M . k = H1(k) from FUNCT_2:sch 4();
 reconsider M = M as sequence of (DualSp X) ;
A2: for k being Nat holds M . k = (F . k) . k
proof
let k be Nat; :: thesis: M . k = (F . k) . k
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
M . k1 = (F . k1) . k1 by A1;
hence M . k = (F . k) . k ; :: thesis: verum
end;
set D = Funcs (NAT,NAT);
reconsider A = N . 0 as Element of Funcs (NAT,NAT) by FUNCT_2:8;
defpred S1[ Nat, sequence of NAT, sequence of NAT] means $3 = $2 * (N . ($1 + 1));
P1: for n being Nat
for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]
let x be Element of Funcs (NAT,NAT); :: thesis: ex y being Element of Funcs (NAT,NAT) st S1[n,x,y]
reconsider y = x * (N . (n + 1)) as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take y ; :: thesis: S1[n,x,y]
thus y = x * (N . (n + 1)) ; :: thesis: verum
end;
consider J being sequence of (Funcs (NAT,NAT)) such that
P2: ( J . 0 = A & ( for n being Nat holds S1[n,J . n,J . (n + 1)] ) ) from RECDEF_1:sch 2(P1);
 defpred S2[ Nat] means J . $1 is V132() sequence of NAT;
Q0: S2[ 0 ] by P2, A0;
Q1: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume X10: S2[n] ; :: thesis: S2[n + 1]
N . (n + 1) is V132() sequence of NAT by A0;
then (J . n) * (N . (n + 1)) is V132() sequence of NAT by X10;
hence J . (n + 1) is V132() sequence of NAT by P2; :: thesis: verum
end;
Q2: for n being Nat holds S2[n] from NAT_1:sch 2(Q0, Q1);
 defpred S3[ Nat] means F . $1 = f * (J . $1);
Q0: S3[ 0 ] by P2, A0;
Q1: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume X2: S3[n] ; :: thesis: S3[n + 1]
F . (n + 1) = (F . n) * (N . (n + 1)) by A0
.= f * ((J . n) * (N . (n + 1))) by X2, RELAT_1:36 ;
hence F . (n + 1) = f * (J . (n + 1)) by P2; :: thesis: verum
end;
A41: for n being Nat holds S3[n] from NAT_1:sch 2(Q0, Q1);
 deffunc H2( Element of NAT ) -> Element of NAT = (J . $1) . $1;
consider L being Function of NAT,NAT such that
A5: for k being Element of NAT holds L . k = H2(k) from FUNCT_2:sch 4();
 reconsider L = L as sequence of NAT ;
A6: for k being Nat holds L . k = (J . k) . k
proof
let k be Nat; :: thesis: L . k = (J . k) . k
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
L . k1 = (J . k1) . k1 by A5;
hence L . k = (J . k) . k ; :: thesis: verum
end;
reconsider L0 = L as Real_Sequence by FUNCT_2:7, NUMBERS:19;
for k being Nat holds L0 . k < L0 . (k + 1)
proof
let k be Nat; :: thesis: L0 . k < L0 . (k + 1)
B2: J . k is V132() Real_Sequence by Q2, FUNCT_2:7, NUMBERS:19;
B3: L . (k + 1) = (J . (k + 1)) . (k + 1) by A6
.= ((J . k) * (N . (k + 1))) . (k + 1) by P2
.= (J . k) . ((N . (k + 1)) . (k + 1)) by FUNCT_2:15 ;
N . (k + 1) is V132() sequence of NAT by A0;
then k + 1 <= (N . (k + 1)) . (k + 1) by SEQM_3:14;
then k < (N . (k + 1)) . (k + 1) by XREAL_1:145;
then (J . k) . k < (J . k) . ((N . (k + 1)) . (k + 1)) by B2, SEQM_3:1;
hence L0 . k < L0 . (k + 1) by B3, A6; :: thesis: verum
end;
then L0 is V132() ;
then reconsider L = L as V132() sequence of NAT ;
for k being Nat holds M . k = (f * L) . k
proof
let k be Nat; :: thesis: M . k = (f * L) . k
M . k = (F . k) . k by A2
.= (f * (J . k)) . k by A41
.= f . ((J . k) . k) by ORDINAL1:def 12, FUNCT_2:15
.= f . (L . k) by A6 ;
hence M . k = (f * L) . k by ORDINAL1:def 12, FUNCT_2:15; :: thesis: verum
end;
then A71: M = f * L ;
for k being Nat holds M # (x . k) is convergent
proof
let k be Nat; :: thesis: M # (x . k) is convergent
Q1: (F . k) # (x . k) is convergent
proof
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: (F . k) # (x . k) is convergent
hence (F . k) # (x . k) is convergent by A0; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: (F . k) # (x . k) is convergent
then ex n being Nat st k = n + 1 by NAT_1:6;
hence (F . k) # (x . k) is convergent by A0; :: thesis: verum
end;
end;
end;
A0X: for k being Nat holds N . k is V132() sequence of NAT
proof
let k be Nat; :: thesis: N . k is V132() sequence of NAT
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: N . k is V132() sequence of NAT
hence N . k is V132() sequence of NAT by A0; :: thesis: verum
end;
end;
end;
defpred S4[ Nat, sequence of NAT] means for i being Nat holds $2 . i = ((N . (k + $1)) . (k + i)) - k;
P11: for n being Element of NAT ex y being Element of Funcs (NAT,NAT) st S4[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,NAT) st S4[n,y]
defpred S5[ Nat, object ] means $2 = ((N . (k + n)) . (k + $1)) - k;
P111: for i being Element of NAT ex y being Element of NAT st S5[i,y]
proof
let i be Element of NAT ; :: thesis: ex y being Element of NAT st S5[i,y]
B5: k <= k + i by NAT_1:11;
N . (k + n) is V132() sequence of NAT by A0X;
then k + i <= (N . (k + n)) . (k + i) by SEQM_3:14;
then k <= (N . (k + n)) . (k + i) by B5, XXREAL_0:2;
then reconsider y = ((N . (k + n)) . (k + i)) - k as Element of NAT by INT_1:3, XREAL_1:48;
take y ; :: thesis: S5[i,y]
thus y = ((N . (k + n)) . (k + i)) - k ; :: thesis: verum
end;
consider y being Function of NAT,NAT such that
P121: for i being Element of NAT holds S5[i,y . i] from FUNCT_2:sch 3(P111);
 reconsider y = y as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take y ; :: thesis: S4[n,y]
thus for i being Nat holds y . i = ((N . (k + n)) . (k + i)) - k :: thesis: verum
proof
let i be Nat; :: thesis: y . i = ((N . (k + n)) . (k + i)) - k
i in NAT by ORDINAL1:def 12;
hence y . i = ((N . (k + n)) . (k + i)) - k by P121; :: thesis: verum
end;
end;
consider Nk being Function of NAT,(Funcs (NAT,NAT)) such that
P12: for n being Element of NAT holds S4[n,Nk . n] from FUNCT_2:sch 3(P11);
 P13: for n being Element of NAT holds Nk . n is V132() sequence of NAT
proof
let n be Element of NAT ; :: thesis: Nk . n is V132() sequence of NAT
reconsider Nkn = Nk . n as Real_Sequence by FUNCT_2:7, NUMBERS:19;
D1: N . (k + n) is V132() Real_Sequence by FUNCT_2:7, NUMBERS:19, A0X;
for i being Nat holds Nkn . i < Nkn . (i + 1)
proof
let i be Nat; :: thesis: Nkn . i < Nkn . (i + 1)
D2: ( (Nk . n) . i = ((N . (k + n)) . (k + i)) - k & (Nk . n) . (i + 1) = ((N . (k + n)) . (k + (i + 1))) - k ) by P12;
((N . (k + n)) . (k + i)) - k < ((N . (k + n)) . ((k + i) + 1)) - k by XREAL_1:14, D1, SEQM_3:def 6;
hence Nkn . i < Nkn . (i + 1) by D2; :: thesis: verum
end;
hence Nk . n is V132() sequence of NAT by SEQM_3:def 6; :: thesis: verum
end;
A0k: for n being Nat holds (F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1))
proof
let n be Nat; :: thesis: (F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1))
XX1: F . ((k + 1) + n) = (F . (k + n)) * (N . ((k + n) + 1)) by A0;
for i being Nat holds (((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i = (((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i
proof
let i be Nat; :: thesis: (((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i = (((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i
N3: (Nk . (n + 1)) . i = ((N . (k + (n + 1))) . (k + i)) - k by P12;
thus (((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i = ((F . (k + n)) ^\ k) . ((Nk . (n + 1)) . i) by FUNCT_2:15, ORDINAL1:def 12
.= (F . (k + n)) . (k + (((N . (k + (n + 1))) . (k + i)) - k)) by NAT_1:def 3, N3
.= ((F . (k + n)) * (N . (k + (n + 1)))) . (k + i) by FUNCT_2:15, ORDINAL1:def 12
.= (((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i by NAT_1:def 3 ; :: thesis: verum
end;
hence (F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1)) by XX1; :: thesis: verum
end;
reconsider Ak = id NAT as Element of Funcs (NAT,NAT) by FUNCT_2:8;
defpred S5[ Nat, sequence of NAT, sequence of NAT] means $3 = $2 * (Nk . ($1 + 1));
P14: for n being Nat
for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S5[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of Funcs (NAT,NAT) ex y being Element of Funcs (NAT,NAT) st S5[n,x,y]
let x be Element of Funcs (NAT,NAT); :: thesis: ex y being Element of Funcs (NAT,NAT) st S5[n,x,y]
reconsider y = x * (Nk . (n + 1)) as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take y ; :: thesis: S5[n,x,y]
thus y = x * (Nk . (n + 1)) ; :: thesis: verum
end;
consider Jk being sequence of (Funcs (NAT,NAT)) such that
P15: ( Jk . 0 = Ak & ( for n being Nat holds S5[n,Jk . n,Jk . (n + 1)] ) ) from RECDEF_1:sch 2(P14);
 defpred S6[ Nat] means Jk . $1 is V132() sequence of NAT;
QJ0: S6[ 0 ] by P15;
QJ1: for n being Nat st S6[n] holds
S6[n + 1]
proof
let n be Nat; :: thesis: ( S6[n] implies S6[n + 1] )
assume X10: S6[n] ; :: thesis: S6[n + 1]
Nk . (n + 1) is V132() sequence of NAT by P13;
then (Jk . n) * (Nk . (n + 1)) is V132() sequence of NAT by X10;
hence Jk . (n + 1) is V132() sequence of NAT by P15; :: thesis: verum
end;
AJ32: for n being Nat holds S6[n] from NAT_1:sch 2(QJ0, QJ1);
 defpred S7[ Nat] means (F . (k + $1)) ^\ k = ((F . k) ^\ k) * (Jk . $1);
QJ0: S7[ 0 ] by P15, FUNCT_2:17;
QJ1: for n being Nat st S7[n] holds
S7[n + 1]
proof
let n be Nat; :: thesis: ( S7[n] implies S7[n + 1] )
assume X2: S7[n] ; :: thesis: S7[n + 1]
thus (F . (k + (n + 1))) ^\ k = ((F . (k + n)) ^\ k) * (Nk . (n + 1)) by A0k
.= ((F . k) ^\ k) * ((Jk . n) * (Nk . (n + 1))) by X2, RELAT_1:36
.= ((F . k) ^\ k) * (Jk . (n + 1)) by P15 ; :: thesis: verum
end;
BJ4: for n being Nat holds S7[n] from NAT_1:sch 2(QJ0, QJ1);
 deffunc H3( Element of NAT ) -> Element of NAT = (Jk . $1) . $1;
consider Lk being Function of NAT,NAT such that
AJ5: for n being Element of NAT holds Lk . n = H3(n) from FUNCT_2:sch 4();
 reconsider Lk = Lk as sequence of NAT ;
AJ6: for k being Nat holds Lk . k = (Jk . k) . k
proof
let k be Nat; :: thesis: Lk . k = (Jk . k) . k
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
Lk . k1 = (Jk . k1) . k1 by AJ5;
hence Lk . k = (Jk . k) . k ; :: thesis: verum
end;
reconsider L0k = Lk as Real_Sequence by FUNCT_2:7, NUMBERS:19;
for k being Nat holds L0k . k < L0k . (k + 1)
proof
let k be Nat; :: thesis: L0k . k < L0k . (k + 1)
B2: Jk . k is V132() Real_Sequence by AJ32, FUNCT_2:7, NUMBERS:19;
B3: Lk . (k + 1) = (Jk . (k + 1)) . (k + 1) by AJ6
.= ((Jk . k) * (Nk . (k + 1))) . (k + 1) by P15
.= (Jk . k) . ((Nk . (k + 1)) . (k + 1)) by FUNCT_2:15 ;
Nk . (k + 1) is V132() sequence of NAT by P13;
then k + 1 <= (Nk . (k + 1)) . (k + 1) by SEQM_3:14;
then k < (Nk . (k + 1)) . (k + 1) by XREAL_1:145;
then (Jk . k) . k < (Jk . k) . ((Nk . (k + 1)) . (k + 1)) by B2, SEQM_3:1;
hence L0k . k < L0k . (k + 1) by B3, AJ6; :: thesis: verum
end;
then L0k is V132() ;
then reconsider Lk = Lk as V132() sequence of NAT ;
for n being Nat holds (M ^\ k) . n = (((F . k) ^\ k) * Lk) . n
proof
let n be Nat; :: thesis: (M ^\ k) . n = (((F . k) ^\ k) * Lk) . n
thus (M ^\ k) . n = M . (k + n) by NAT_1:def 3
.= (F . (k + n)) . (k + n) by A2
.= ((F . (k + n)) ^\ k) . n by NAT_1:def 3
.= (((F . k) ^\ k) * (Jk . n)) . n by BJ4
.= ((F . k) ^\ k) . ((Jk . n) . n) by ORDINAL1:def 12, FUNCT_2:15
.= ((F . k) ^\ k) . (Lk . n) by AJ6
.= (((F . k) ^\ k) * Lk) . n by ORDINAL1:def 12, FUNCT_2:15 ; :: thesis: verum
end;
then P11: M ^\ k = ((F . k) ^\ k) * Lk ;
Q12: for n being Nat holds ((M ^\ k) # (x . k)) . n = ((M # (x . k)) ^\ k) . n
proof
let n be Nat; :: thesis: ((M ^\ k) # (x . k)) . n = ((M # (x . k)) ^\ k) . n
thus ((M ^\ k) # (x . k)) . n = ((M ^\ k) . n) . (x . k) by Def1
.= (M . (k + n)) . (x . k) by NAT_1:def 3
.= (M # (x . k)) . (k + n) by Def1
.= ((M # (x . k)) ^\ k) . n by NAT_1:def 3 ; :: thesis: verum
end;
for n being Nat holds ((((F . k) ^\ k) * Lk) # (x . k)) . n = ((((F . k) ^\ k) # (x . k)) * Lk) . n
proof
let n be Nat; :: thesis: ((((F . k) ^\ k) * Lk) # (x . k)) . n = ((((F . k) ^\ k) # (x . k)) * Lk) . n
thus ((((F . k) ^\ k) * Lk) # (x . k)) . n = ((((F . k) ^\ k) * Lk) . n) . (x . k) by Def1
.= (((F . k) ^\ k) . (Lk . n)) . (x . k) by ORDINAL1:def 12, FUNCT_2:15
.= (((F . k) ^\ k) # (x . k)) . (Lk . n) by Def1
.= ((((F . k) ^\ k) # (x . k)) * Lk) . n by ORDINAL1:def 12, FUNCT_2:15 ; :: thesis: verum
end;
then (((F . k) ^\ k) * Lk) # (x . k) = (((F . k) ^\ k) # (x . k)) * Lk ;
then Q2: (M # (x . k)) ^\ k = (((F . k) ^\ k) # (x . k)) * Lk by P11, Q12;
for n being Nat holds (((F . k) # (x . k)) ^\ k) . n = (((F . k) ^\ k) # (x . k)) . n
proof
let n be Nat; :: thesis: (((F . k) # (x . k)) ^\ k) . n = (((F . k) ^\ k) # (x . k)) . n
thus (((F . k) # (x . k)) ^\ k) . n = ((F . k) # (x . k)) . (k + n) by NAT_1:def 3
.= ((F . k) . (k + n)) . (x . k) by Def1
.= (((F . k) ^\ k) . n) . (x . k) by NAT_1:def 3
.= (((F . k) ^\ k) # (x . k)) . n by Def1 ; :: thesis: verum
end;
then ((F . k) # (x . k)) ^\ k = ((F . k) ^\ k) # (x . k) ;
then (M # (x . k)) ^\ k is convergent by Q1, Q2, SEQ_4:16;
hence M # (x . k) is convergent by SEQ_4:21; :: thesis: verum
end;
hence ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) ) by A71; :: thesis: verum