let X be RealBanachSpace; :: thesis: for f being sequence of (DualSp X) st X is separable & ||.f.|| is bounded holds
ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )
let f be sequence of (DualSp X); :: thesis: ( X is separable & ||.f.|| is bounded implies ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent ) )
assume that
A1: X is separable and
A2: ||.f.|| is bounded ; :: thesis: ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )
consider x0 being sequence of X such that
A3: rng x0 is dense by A1, NORMSP_3:21;
set X0 = rng x0;
consider f0 being sequence of (DualSp X) such that
AX: f0 is subsequence of f and
A31: for n being Nat holds f0 # (x0 . n) is convergent by A2, Lm814;
A21: for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds |.((f # x) . n).| <= K ) )

proof

let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for n being Nat holds |.((f # x) . n).| <= K ) )
consider K0 being Real such that
B0: ( 0 < K0 & ( for n being Nat holds |.(||.f.|| . n).| < K0 ) ) by A2, SEQ_2:3;
reconsider K = (K0 * ||.x.||) + 1 as Real ;
take K ; :: thesis: ( 0 <= K & ( for n being Nat holds |.((f # x) . n).| <= K ) )
B11: (K0 * ||.x.||) + 0 < (K0 * ||.x.||) + 1 by XREAL_1:8;
thus 0 <= K by B0; :: thesis: for n being Nat holds |.((f # x) . n).| <= K
thus for n being Nat holds |.((f # x) . n).| <= K :: thesis: verum

proof

let n be Nat; :: thesis: |.((f # x) . n).| <= K
B2: |.(||.f.|| . n).| <= K0 by B0;
||.f.|| . n = ||.(f . n).|| by NORMSP_0:def 4;
then B3: ||.(f . n).|| <= K0 by B2, ABSVALUE:def 1;
reconsider h = f . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B4: |.(h . x).| <= ||.(f . n).|| * ||.x.|| by DUALSP01:26;
B51: ||.(f . n).|| * ||.x.|| <= K0 * ||.x.|| by B3, XREAL_1:64;
|.((f # x) . n).| = |.((f . n) . x).| by Def1;
then |.((f # x) . n).| <= K0 * ||.x.|| by B51, B4, XXREAL_0:2;
hence |.((f # x) . n).| <= K by B11, XXREAL_0:2; :: thesis: verum

end;

end;

set T = rng f0;
consider N being increasing sequence of NAT such that
AY: f0 = f * N by AX, VALUED_0:def 17;
for x being Point of X ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f0 holds
|.(g . x).| <= K ) )

proof

let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f0 holds
|.(g . x).| <= K ) )
consider K being Real such that
A4: ( 0 <= K & ( for n being Nat holds |.((f # x) . n).| <= K ) ) by A21;
A5: for n being Nat holds |.((f0 # x) . n).| <= K

proof

let n be Nat; :: thesis: |.((f0 # x) . n).| <= K
B3: f0 . n = f . (N . n) by AY, ORDINAL1:def 12, FUNCT_2:15;
reconsider n0 = N . n as Nat ;
(f0 # x) . n = (f0 . n) . x by Def1
.= (f # x) . n0 by B3, Def1 ;
hence |.((f0 # x) . n).| <= K by A4; :: thesis: verum

end;

for g being Point of (DualSp X) st g in rng f0 holds
|.(g . x).| <= K

proof

let g be Point of (DualSp X); :: thesis: ( g in rng f0 implies |.(g . x).| <= K )
assume g in rng f0 ; :: thesis: |.(g . x).| <= K
then consider n being object such that
B1: ( n in NAT & g = f0 . n ) by FUNCT_2:11;
reconsider n = n as Nat by B1;
g . x = (f0 # x) . n by B1, Def1;
hence |.(g . x).| <= K by A5; :: thesis: verum

end;

hence ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f0 holds
|.(g . x).| <= K ) ) by A4; :: thesis: verum

end;

then consider L being Real such that
A7: ( 0 <= L & ( for g being Point of (DualSp X) st g in rng f0 holds
||.g.|| <= L ) ) by Lm55;
set M = L + 1;
A8: L + 0 < L + 1 by XREAL_1:8;
A9: for g being Lipschitzian linear-Functional of X st g in rng f0 holds
for x, y being Point of X holds |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).||

proof

let g be Lipschitzian linear-Functional of X; :: thesis: ( g in rng f0 implies for x, y being Point of X holds |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).|| )
reconsider g1 = g as Point of (DualSp X) by DUALSP01:def 10;
assume g in rng f0 ; :: thesis: for x, y being Point of X holds |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).||
then ||.g1.|| <= L by A7;
then B1: ||.g1.|| < L + 1 by A8, XXREAL_0:2;
let x, y be Point of X; :: thesis: |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).||
|.((g . x) - (g . y)).| = |.((g . x) + ((- 1) * (g . y))).| ;
then |.((g . x) - (g . y)).| = |.((g . x) + (g . ((- 1) * y))).| by HAHNBAN:def 3;
then |.((g . x) - (g . y)).| = |.(g . (x + ((- 1) * y))).| by HAHNBAN:def 2;
then B2: |.((g . x) - (g . y)).| = |.(g . (x - y)).| by RLVECT_1:16;
B3: |.(g . (x - y)).| <= ||.g1.|| * ||.(x - y).|| by DUALSP01:26;
||.g1.|| * ||.(x - y).|| <= (L + 1) * ||.(x - y).|| by B1, XREAL_1:64;
hence |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).|| by B2, B3, XXREAL_0:2; :: thesis: verum

end;

BX: for x being Point of X holds f0 # x is convergent

proof

let x be Point of X; :: thesis: f0 # x is convergent
for TK1 being Real st TK1 > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1

proof

let TK1 be Real; :: thesis: ( TK1 > 0 implies ex m being Nat st
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 )
assume B1: TK1 > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
then C2: 0 < TK1 / (3 * (L + 1)) by A7;
set V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } ;
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } c= the carrier of X

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } or s in the carrier of X )
assume s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } ; :: thesis: s in the carrier of X
then ex z being Point of X st
( s = z & ||.(x - z).|| < TK1 / (3 * (L + 1)) ) ;
hence s in the carrier of X ; :: thesis: verum

end;

then reconsider V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } as Subset of X ;
reconsider TKK = TK1 as Real ;
V is open Subset of (TopSpaceNorm X) by NORMSP_2:8;
then B31: V is open by NORMSP_2:16;
||.(x - x).|| < TKK / (3 * (L + 1)) by C2, NORMSP_1:6;
then x in V ;
then consider s being object such that
B3: ( s in rng x0 & s in V ) by XBOOLE_0:3, B31, A3, NORMSP_3:17;
consider y being Point of X such that
B4: ( s = y & ||.(x - y).|| < TK1 / (3 * (L + 1)) ) by B3;
consider m being Element of NAT such that
B40: s = x0 . m by B3, FUNCT_2:113;
consider m being Nat such that
B5: for n being Nat st m <= n holds
|.(((f0 # y) . n) - ((f0 # y) . m)).| < TK1 / 3 by B1, A31, SEQ_4:41, B4, B40;
take m ; :: thesis: for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1

proof

let n be Nat; :: thesis: ( n >= m implies |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 )
B6: m in NAT by ORDINAL1:def 12;
B7: n in NAT by ORDINAL1:def 12;
reconsider g = f0 . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
reconsider h = f0 . m as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B8: |.(((f0 # x) . n) - ((f0 # y) . m)).| + |.(((f0 # y) . m) - ((f0 # x) . m)).| <= (|.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).| by XREAL_1:6, COMPLEX1:63;
assume n >= m ; :: thesis: |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
then |.(((f0 # y) . n) - ((f0 # y) . m)).| < TK1 / 3 by B5;
then |.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).| < |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3) by XREAL_1:8;
then B9: (|.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).| < (|.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| by XREAL_1:8;
|.(((f0 # x) . m) - ((f0 # y) . m)).| = |.(((f0 . m) . x) - ((f0 # y) . m)).| by Def1;
then |.(((f0 # x) . m) - ((f0 # y) . m)).| = |.((h . x) - (h . y)).| by Def1;
then B10: |.(((f0 # x) . m) - ((f0 # y) . m)).| <= (L + 1) * ||.(x - y).|| by A9, FUNCT_2:4, B6;
(L + 1) * ||.(x - y).|| < (L + 1) * (TK1 / (3 * (L + 1))) by A7, B4, XREAL_1:68;
then (L + 1) * ||.(x - y).|| < TK1 / 3 by A7, XCMPLX_1:92;
then |.(((f0 # x) . m) - ((f0 # y) . m)).| < TK1 / 3 by B10, XXREAL_0:2;
then |.(((f0 # y) . m) - ((f0 # x) . m)).| < TK1 / 3 by COMPLEX1:60;
then B11: ((TK1 / 3) + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by XREAL_1:8;
|.(((f0 # x) . n) - ((f0 # y) . n)).| = |.(((f0 . n) . x) - ((f0 # y) . n)).| by Def1;
then |.(((f0 # x) . n) - ((f0 # y) . n)).| = |.((g . x) - (g . y)).| by Def1;
then B12: |.(((f0 # x) . n) - ((f0 # y) . n)).| <= (L + 1) * ||.(x - y).|| by A9, FUNCT_2:4, B7;
|.(((f0 # x) . n) - ((f0 # x) . m)).| <= |.(((f0 # x) . n) - ((f0 # y) . m)).| + |.(((f0 # y) . m) - ((f0 # x) . m)).| by COMPLEX1:63;
then |.(((f0 # x) . n) - ((f0 # x) . m)).| <= (|.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).| by B8, XXREAL_0:2;
then B13: |.(((f0 # x) . n) - ((f0 # x) . m)).| < (|.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| by B9, XXREAL_0:2;
(L + 1) * ||.(x - y).|| < (L + 1) * (TK1 / (3 * (L + 1))) by A7, B4, XREAL_1:68;
then (L + 1) * ||.(x - y).|| < TK1 / 3 by A7, XCMPLX_1:92;
then |.(((f0 # x) . n) - ((f0 # y) . n)).| < TK1 / 3 by B12, XXREAL_0:2;
then |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3) < (TK1 / 3) + (TK1 / 3) by XREAL_1:8;
then (|.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| < ((TK1 / 3) + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| by XREAL_1:8;
then (|.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by B11, XXREAL_0:2;
hence |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 by B13, XXREAL_0:2; :: thesis: verum

end;

hence for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 ; :: thesis: verum

end;

hence f0 # x is convergent by SEQ_4:41; :: thesis: verum

end;

defpred S₁[ Element of the carrier of X, object ] means $2 = lim (f0 # $1);
C01: for x being Element of the carrier of X ex y being Element of REAL st S₁[x,y]

proof

let x be Element of the carrier of X; :: thesis: ex y being Element of REAL st S₁[x,y]
lim (f0 # x) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S₁[x,y] ; :: thesis: verum

end;

consider f1 being Function of the carrier of X,REAL such that
C0: for x being Element of the carrier of X holds S₁[x,f1 . x] from FUNCT_2:sch 3(C01);
C2: f1 is additive

proof

let x, y be Point of X; :: according to HAHNBAN:def 2 :: thesis: f1 . (x + y) = K55((f1 . x),(f1 . y))

D11: now :: thesis: for n being Nat holds (f0 # (x + y)) . n = ((f0 # x) . n) + ((f0 # y) . n)

let n be Nat; :: thesis: (f0 # (x + y)) . n = ((f0 # x) . n) + ((f0 # y) . n)
reconsider h = f0 . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
thus (f0 # (x + y)) . n = (f0 . n) . (x + y) by Def1
.= (h . x) + (h . y) by HAHNBAN:def 2
.= ((f0 # x) . n) + ((f0 . n) . y) by Def1
.= ((f0 # x) . n) + ((f0 # y) . n) by Def1 ; :: thesis: verum

end;

D2: ( f0 # x is convergent & f0 # y is convergent ) by BX;
thus f1 . (x + y) = lim (f0 # (x + y)) by C0
.= lim ((f0 # x) + (f0 # y)) by D11, SEQ_1:7
.= (lim (f0 # x)) + (lim (f0 # y)) by D2, SEQ_2:6
.= (f1 . x) + (lim (f0 # y)) by C0
.= (f1 . x) + (f1 . y) by C0 ; :: thesis: verum

end;

C31: f1 is homogeneous

proof

let x be Point of X; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f1 . (b₁ * x) = b₁ * (f1 . x)
let r be Real; :: thesis: f1 . (r * x) = r * (f1 . x)

D31: now :: thesis: for n being Nat holds (f0 # (r * x)) . n = r * ((f0 # x) . n)

let n be Nat; :: thesis: (f0 # (r * x)) . n = r * ((f0 # x) . n)
reconsider h = f0 . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
thus (f0 # (r * x)) . n = (f0 . n) . (r * x) by Def1
.= r * (h . x) by HAHNBAN:def 3
.= r * ((f0 # x) . n) by Def1 ; :: thesis: verum

end;

thus f1 . (r * x) = lim (f0 # (r * x)) by C0
.= lim (r (#) (f0 # x)) by D31, SEQ_1:9
.= r * (lim (f0 # x)) by BX, SEQ_2:8
.= r * (f1 . x) by C0 ; :: thesis: verum

end;

consider M being Real such that
C4: ( 0 < M & ( for n being Nat holds |.(||.f.|| . n).| < M ) ) by A2, SEQ_2:3;

now :: thesis: for x being Point of X holds |.(f1 . x).| <= M * ||.x.||

let x be Point of X; :: thesis: |.(f1 . x).| <= M * ||.x.||
D5: f0 # x is convergent by BX;
D7: |.(f1 . x).| = |.(lim (f0 # x)).| by C0
.= lim |.(f0 # x).| by BX, SEQ_4:14 ;
D8: for n being Nat holds ||.(f0 . n).|| <= M

proof

let n be Nat; :: thesis: ||.(f0 . n).|| <= M
f0 . n = f . (N . n) by AY, ORDINAL1:def 12, FUNCT_2:15;
then E3: ||.(f0 . n).|| = ||.f.|| . (N . n) by NORMSP_0:def 4;
|.(||.f.|| . (N . n)).| < M by C4;
hence ||.(f0 . n).|| <= M by E3, ABSVALUE:def 1; :: thesis: verum

end;

reconsider s = M * ||.x.|| as Real ;

D91: now :: thesis: for n being Nat holds |.(f0 # x).| . n <= (seq_const s) . n

let n be Nat; :: thesis: |.(f0 # x).| . n <= (seq_const s) . n
reconsider h = f0 . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
E3: |.(h . x).| <= ||.(f0 . n).|| * ||.x.|| by DUALSP01:26;
||.(f0 . n).|| * ||.x.|| <= M * ||.x.|| by XREAL_1:64, D8;
then |.(h . x).| <= M * ||.x.|| by E3, XXREAL_0:2;
then E51: |.((f0 # x) . n).| <= M * ||.x.|| by Def1;
(seq_const s) . n = s by SEQ_1:57;
hence |.(f0 # x).| . n <= (seq_const s) . n by E51, SEQ_1:12; :: thesis: verum

end;

lim (seq_const s) = (seq_const s) . 0 by SEQ_4:26
.= s ;
hence |.(f1 . x).| <= M * ||.x.|| by D7, D91, D5, SEQ_2:18; :: thesis: verum

end;

then f1 is Lipschitzian by C4;
then f1 is Point of (DualSp X) by DUALSP01:def 10, C31, C2;
then f0 is weakly*-convergent by BX, C0;
hence ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent ) by AX; :: thesis: verum