let X be RealNormSpace; for seq being sequence of (DualSp X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (DualSp X); ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2:
vseq is Cauchy_sequence_by_Norm
; vseq is convergent
defpred S1[ set , set ] means ex xseq being sequence of REAL st
( ( for n being Nat holds xseq . n = (Bound2Lipschitz ((vseq . n),X)) . $1 ) & xseq is convergent & $2 = lim xseq );
A3:
for x being Element of X ex y being Element of REAL st S1[x,y]
consider f being Function of the carrier of X,REAL such that
A20:
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of the carrier of X,REAL ;
A21:
now for x, y being VECTOR of X holds tseq . (x + y) = (tseq . x) + (tseq . y)end;
then reconsider tseq = tseq as linear-Functional of X by A21, HAHNBAN:def 2, HAHNBAN:def 3;
then A40:
||.vseq.|| is convergent
by SEQ_4:41;
A41:
tseq is Lipschitzian
A54:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||
reconsider tseq = tseq as Lipschitzian linear-Functional of X by A41;
reconsider tv = tseq as Point of (DualSp X) by Def9;
A72:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
hence
vseq is convergent
; verum