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 increasing 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 increasing sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) ) by Lm814C;
deffunc H₁( 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 = H₁(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 S₁[ 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 S₁[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 S₁[n,x,y]
let x be Element of Funcs (NAT,NAT); :: thesis: ex y being Element of Funcs (NAT,NAT) st S₁[n,x,y]
reconsider y = x * (N . (n + 1)) as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take y ; :: thesis: S₁[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 S₁[n,J . n,J . (n + 1)] ) ) from RECDEF_1:sch 2(P1);
defpred S₂[ Nat] means J . $1 is increasing sequence of NAT;
Q0: S₂[ 0 ] by P2, A0;
Q1: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume X10: S₂[n] ; :: thesis: S₂[n + 1]
N . (n + 1) is increasing sequence of NAT by A0;
then (J . n) * (N . (n + 1)) is increasing sequence of NAT by X10;
hence J . (n + 1) is increasing sequence of NAT by P2; :: thesis: verum

end;

Q2: for n being Nat holds S₂[n] from NAT_1:sch 2(Q0, Q1);
defpred S₃[ Nat] means F . $1 = f * (J . $1);
Q0: S₃[ 0 ] by P2, A0;
Q1: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume X2: S₃[n] ; :: thesis: S₃[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 S₃[n] from NAT_1:sch 2(Q0, Q1);
deffunc H₂( 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 = H₂(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 increasing 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 increasing 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 increasing ;
then reconsider L = L as increasing 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 increasing sequence of NAT

proof

let k be Nat; :: thesis: N . k is increasing sequence of NAT

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: N . k is increasing sequence of NAT

hence N . k is increasing sequence of NAT by A0; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: N . k is increasing sequence of NAT

then ex n being Nat st k = n + 1 by NAT_1:6;
hence N . k is increasing sequence of NAT by A0; :: thesis: verum

end;

end;

end;

defpred S₄[ 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 S₄[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,NAT) st S₄[n,y]
defpred S₅[ Nat, object ] means $2 = ((N . (k + n)) . (k + $1)) - k;
P111: for i being Element of NAT ex y being Element of NAT st S₅[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of NAT st S₅[i,y]
B5: k <= k + i by NAT_1:11;
N . (k + n) is increasing 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: S₅[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 S₅[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: S₄[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 S₄[n,Nk . n] from FUNCT_2:sch 3(P11);
P13: for n being Element of NAT holds Nk . n is increasing sequence of NAT

proof

let n be Element of NAT ; :: thesis: Nk . n is increasing sequence of NAT
reconsider Nkn = Nk . n as Real_Sequence by FUNCT_2:7, NUMBERS:19;
D1: N . (k + n) is increasing 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 increasing 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 S₅[ 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 S₅[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 S₅[n,x,y]
let x be Element of Funcs (NAT,NAT); :: thesis: ex y being Element of Funcs (NAT,NAT) st S₅[n,x,y]
reconsider y = x * (Nk . (n + 1)) as Element of Funcs (NAT,NAT) by FUNCT_2:8;
take y ; :: thesis: S₅[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 S₅[n,Jk . n,Jk . (n + 1)] ) ) from RECDEF_1:sch 2(P14);
defpred S₆[ Nat] means Jk . $1 is increasing sequence of NAT;
QJ0: S₆[ 0 ] by P15;
QJ1: for n being Nat st S₆[n] holds
S₆[n + 1]

proof

let n be Nat; :: thesis: ( S₆[n] implies S₆[n + 1] )
assume X10: S₆[n] ; :: thesis: S₆[n + 1]
Nk . (n + 1) is increasing sequence of NAT by P13;
then (Jk . n) * (Nk . (n + 1)) is increasing sequence of NAT by X10;
hence Jk . (n + 1) is increasing sequence of NAT by P15; :: thesis: verum

end;

AJ32: for n being Nat holds S₆[n] from NAT_1:sch 2(QJ0, QJ1);
defpred S₇[ Nat] means (F . (k + $1)) ^\ k = ((F . k) ^\ k) * (Jk . $1);
QJ0: S₇[ 0 ] by P15, FUNCT_2:17;
QJ1: for n being Nat st S₇[n] holds
S₇[n + 1]

proof

let n be Nat; :: thesis: ( S₇[n] implies S₇[n + 1] )
assume X2: S₇[n] ; :: thesis: S₇[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 S₇[n] from NAT_1:sch 2(QJ0, QJ1);
deffunc H₃( 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 = H₃(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 increasing 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 increasing 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 increasing ;
then reconsider Lk = Lk as increasing 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