let X be RealNormSpace; :: thesis: for x being sequence of X st x is convergent holds
( x is weakly-convergent & w-lim x = lim x )
let x be sequence of X; :: thesis: ( x is convergent implies ( x is weakly-convergent & w-lim x = lim x ) )
assume A2: x is convergent ; :: thesis: ( x is weakly-convergent & w-lim x = lim x )
reconsider x0 = lim x as Point of X ;
A3: for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . x0 )

proof

let f be Lipschitzian linear-Functional of X; :: thesis: ( f * x is convergent & lim (f * x) = f . x0 )
B1: dom f = the carrier of X by FUNCT_2:def 1;
consider K being Real such that
B3: ( 0 <= K & ( for x being VECTOR of X holds |.(f . x).| <= K * ||.x.|| ) ) by DUALSP01:def 9;
for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds
|.((f /. x1) - (f /. x2)).| <= (K + 1) * ||.(x1 - x2).||

proof

let x1, x2 be Point of X; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X implies |.((f /. x1) - (f /. x2)).| <= (K + 1) * ||.(x1 - x2).|| )
assume ( x1 in the carrier of X & x2 in the carrier of X ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= (K + 1) * ||.(x1 - x2).||
C2: |.((f /. x1) - (f /. x2)).| = |.(f . (x1 - x2)).| by HAHNBAN:19;
C3: |.(f . (x1 - x2)).| <= K * ||.(x1 - x2).|| by B3;
0 + K <= K + 1 by XREAL_1:8;
then K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by XREAL_1:64;
hence |.((f /. x1) - (f /. x2)).| <= (K + 1) * ||.(x1 - x2).|| by XXREAL_0:2, C2, C3; :: thesis: verum

end;

then f is_Lipschitzian_on the carrier of X by FUNCT_2:def 1, B3;
then f is_continuous_on the carrier of X by NFCONT_1:46;
then B81: f is_continuous_in x0 ;
B6: rng x c= the carrier of X ;
then f /* x = f * x by B1, FUNCT_2:def 11;
hence ( f * x is convergent & lim (f * x) = f . x0 ) by B81, A2, B1, B6; :: thesis: verum

end;

then A4: x is weakly-convergent ;

now :: thesis: for f being Lipschitzian linear-Functional of X holds f . ((w-lim x) - x0) = 0

let f be Lipschitzian linear-Functional of X; :: thesis: f . ((w-lim x) - x0) = 0
f . ((w-lim x) - x0) = (f . (w-lim x)) - (f . x0) by HAHNBAN:19
.= (lim (f * x)) - (f . x0) by A4, DefWeaklim
.= (lim (f * x)) - (lim (f * x)) by A3 ;
hence f . ((w-lim x) - x0) = 0 ; :: thesis: verum

end;

then (w-lim x) - (lim x) = 0. X by DUALSP02:8;
hence ( x is weakly-convergent & w-lim x = lim x ) by A3, RLVECT_1:21; :: thesis: verum