let X be RealBanachSpace; :: thesis: for x being sequence of X st X is Reflexive & ||.x.|| is bounded holds
ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent )
let x be sequence of X; :: thesis: ( X is Reflexive & ||.x.|| is bounded implies ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent ) )
assume that
A2: X is Reflexive and
A3: ||.x.|| is bounded ; :: thesis: ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent )
set L = ClNLin (rng x);
reconsider L0 = the carrier of (ClNLin (rng x)) as Subset of X by DUALSP01:def 16;
LM1: for z being object st z in rng x holds
z in the carrier of (ClNLin (rng x))

proof

let z be object ; :: thesis: ( z in rng x implies z in the carrier of (ClNLin (rng x)) )
assume z in rng x ; :: thesis: z in the carrier of (ClNLin (rng x))
then C14: z in Lin (rng x) by RLVECT_3:15;
ex Z being Subset of X st
( Z = the carrier of (Lin (rng x)) & ClNLin (rng x) = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by NORMSP_3:def 20;
hence z in the carrier of (ClNLin (rng x)) by NORMSP_3:4, C14, TARSKI:def 3; :: thesis: verum

end;

per cases ( rng x c= {(0. X)} or not rng x c= {(0. X)} ) ;

suppose XX1: rng x c= {(0. X)} ; :: thesis: ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent )

take x ; :: thesis: ( x is subsequence of x & x is weakly-convergent )
thus x is subsequence of x by VALUED_0:19; :: thesis: x is weakly-convergent
thus x is weakly-convergent by XX1, WEAKLM1; :: thesis: verum

end;

suppose not rng x c= {(0. X)} ; :: thesis: ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent )

then consider z being object such that
B11: ( z in rng x & not z in {(0. X)} ) ;
B12: ( z in rng x & z <> 0. X ) by B11, TARSKI:def 1;
B17: z in the carrier of (ClNLin (rng x)) by LM1, B11;
0. X = 0. (ClNLin (rng x)) by DUALSP01:def 16;
then A11: not ClNLin (rng x) is trivial by B12, B17;
A12: ClNLin (rng x) is Reflexive by A2, NORMSP_4:29;
DualSp (DualSp (ClNLin (rng x))) is separable by A11, A12, NORMSP_4:25;
then A4: DualSp (ClNLin (rng x)) is separable by Th73;
set F = BidualFunc (ClNLin (rng x));
rng x c= the carrier of (ClNLin (rng x)) by LM1;
then reconsider x1 = x as sequence of (ClNLin (rng x)) by FUNCT_2:6;
for i being Nat holds ||.x1.|| . i = ||.x.|| . i

proof

let i be Nat; :: thesis: ||.x1.|| . i = ||.x.|| . i
thus ||.x1.|| . i = ||.(x1 . i).|| by NORMSP_0:def 4
.= ||.(x . i).|| by NORMSP_3:28
.= ||.x.|| . i by NORMSP_0:def 4 ; :: thesis: verum

end;

then B13: ||.x1.|| = ||.x.|| ;
then consider r being Real such that
A5: for n being Nat holds ||.x1.|| . n < r by A3, SEQ_2:def 3;
for n being Nat holds ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n < r

proof

let n be Nat; :: thesis: ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n < r
C2: ||.x1.|| . n < r by A5;
||.(x1 . n).|| = ||.((BidualFunc (ClNLin (rng x))) . (x1 . n)).|| by A11, DUALSP02:9;
then ||.((BidualFunc (ClNLin (rng x))) . (x1 . n)).|| < r by C2, NORMSP_0:def 4;
then ||.(((BidualFunc (ClNLin (rng x))) * x1) . n).|| < r by ORDINAL1:def 12, FUNCT_2:15;
hence ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n < r by NORMSP_0:def 4; :: thesis: verum

end;

then A6: ||.((BidualFunc (ClNLin (rng x))) * x1).|| is bounded_above ;
consider s being Real such that
A7: for n being Nat holds s < ||.x1.|| . n by B13, A3, SEQ_2:def 4;
for n being Nat holds s < ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n

proof

let n be Nat; :: thesis: s < ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n
C4: s < ||.x1.|| . n by A7;
||.(x1 . n).|| = ||.((BidualFunc (ClNLin (rng x))) . (x1 . n)).|| by A11, DUALSP02:9;
then s < ||.((BidualFunc (ClNLin (rng x))) . (x1 . n)).|| by C4, NORMSP_0:def 4;
then s < ||.(((BidualFunc (ClNLin (rng x))) * x1) . n).|| by ORDINAL1:def 12, FUNCT_2:15;
hence s < ||.((BidualFunc (ClNLin (rng x))) * x1).|| . n by NORMSP_0:def 4; :: thesis: verum

end;

then ||.((BidualFunc (ClNLin (rng x))) * x1).|| is bounded_below ;
then consider f1 being sequence of (DualSp (DualSp (ClNLin (rng x)))) such that
A9: ( f1 is subsequence of (BidualFunc (ClNLin (rng x))) * x1 & f1 is weakly*-convergent ) by A4, A6, Th814;
consider L1 being increasing sequence of NAT such that
A91: f1 = ((BidualFunc (ClNLin (rng x))) * x1) * L1 by A9, VALUED_0:def 17;
reconsider x01 = x1 * L1 as sequence of (ClNLin (rng x)) ;
f1 = (BidualFunc (ClNLin (rng x))) * x01 by A91, RELAT_1:36;
then HX: x01 is weakly-convergent by A9, A12, Lm813A;
BX: the carrier of (ClNLin (rng x)) c= the carrier of X by DUALSP01:def 16;
then reconsider x0 = x01 as sequence of X by FUNCT_2:7;
reconsider y = w-lim x01 as Point of X by BX;
for h being Lipschitzian linear-Functional of X holds
( h * x0 is convergent & lim (h * x0) = h . y )

proof

let h be Lipschitzian linear-Functional of X; :: thesis: ( h * x0 is convergent & lim (h * x0) = h . y )
reconsider h1 = h | the carrier of (ClNLin (rng x)) as Lipschitzian linear-Functional of (ClNLin (rng x)) by NORMSP_4:22;
GX3: dom h1 = the carrier of (ClNLin (rng x)) by FUNCT_2:def 1;
then rng x01 c= dom h1 ;
then GX2: h1 * x01 = h * x0 by RELAT_1:165;
( h1 * x01 is convergent & lim (h1 * x01) = h1 . (w-lim x01) ) by HX, DefWeaklim;
hence ( h * x0 is convergent & lim (h * x0) = h . y ) by GX2, GX3, FUNCT_1:47; :: thesis: verum

end;

then x0 is weakly-convergent ;
hence ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent ) ; :: thesis: verum

end;

end;