let X be RealNormSpace; :: thesis: for x being sequence of X st rng x c= {(0. X)} holds
x is weakly-convergent
let x be sequence of X; :: thesis: ( rng x c= {(0. X)} implies x is weakly-convergent )
assume AS: rng x c= {(0. X)} ; :: thesis: x is weakly-convergent
reconsider x0 = 0. X as Point of X ;
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 )
A2: for p being Real
for n being Nat st 0 < p holds
|.(((f * x) . n) - (f . x0)).| < p

proof

let p be Real; :: thesis: for n being Nat st 0 < p holds
|.(((f * x) . n) - (f . x0)).| < p
let n be Nat; :: thesis: ( 0 < p implies |.(((f * x) . n) - (f . x0)).| < p )
assume AS1: 0 < p ; :: thesis: |.(((f * x) . n) - (f . x0)).| < p
C21: x . n in rng x by FUNCT_2:4, ORDINAL1:def 12;
(f * x) . n = f . (x . n) by ORDINAL1:def 12, FUNCT_2:15;
then (f * x) . n = f . (0. X) by TARSKI:def 1, AS, C21;
hence |.(((f * x) . n) - (f . x0)).| < p by AS1, COMPLEX1:44; :: thesis: verum

end;

A1: for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((f * x) . n) - (f . x0)).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
|.(((f * x) . n) - (f . x0)).| < p )
assume AS1: 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((f * x) . n) - (f . x0)).| < p
take m = 0 ; :: thesis: for n being Nat st m <= n holds
|.(((f * x) . n) - (f . x0)).| < p
thus for n being Nat st m <= n holds
|.(((f * x) . n) - (f . x0)).| < p by AS1, A2; :: thesis: verum

end;

then f * x is convergent ;
hence ( f * x is convergent & lim (f * x) = f . x0 ) by A1, SEQ_2:def 7; :: thesis: verum

end;

hence x is weakly-convergent ; :: thesis: verum