let X be RealNormSpace; :: thesis: 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); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
defpred S₁[ 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 S₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of REAL st S₁[x,y]
deffunc H₁( Nat) -> Element of REAL = (Bound2Lipschitz ((vseq . $1),X)) . x;
consider xseq being Real_Sequence such that
A4: for n being Nat holds xseq . n = H₁(n) from SEQ_1:sch 1();
reconsider y = lim xseq as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S₁[x,y]
A6: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||

proof

let m, k be Nat; :: thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian linear-Functional of X by Def9;
A7: ( xseq . k = (Bound2Lipschitz ((vseq . k),X)) . x & xseq . m = (Bound2Lipschitz ((vseq . m),X)) . x ) by A4;
( vseq . m is Lipschitzian linear-Functional of X & vseq . k is Lipschitzian linear-Functional of X ) by Def9;
then ( Bound2Lipschitz ((vseq . m),X) = vseq . m & Bound2Lipschitz ((vseq . k),X) = vseq . k ) by Th29;
then (xseq . m) - (xseq . k) = h1 . x by A7, Th40;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th32; :: thesis: verum

end;

now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st b₃ >= n holds
|.((xseq . b₃) - (xseq . n)).| < k )
assume A10: e > 0 ; :: thesis: ex k being Nat st
for n being Nat st b₃ >= n holds
|.((xseq . b₃) - (xseq . n)).| < k

per cases ( x = 0. X or x <> 0. X ) ;

suppose A11: x = 0. X ; :: thesis: ex k being Nat st
for n being Nat st b₃ >= n holds
|.((xseq . b₃) - (xseq . n)).| < k

reconsider k = 0 as Nat ;
take k = k; :: thesis: for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
thus for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e :: thesis: verum

proof

let n be Nat; :: thesis: ( n >= k implies |.((xseq . n) - (xseq . k)).| < e )
assume n >= k ; :: thesis: |.((xseq . n) - (xseq . k)).| < e
A12: xseq . k = (Bound2Lipschitz ((vseq . k),X)) . (0 * x) by A4, A11
.= 0 * ((Bound2Lipschitz ((vseq . k),X)) . x) by HAHNBAN:def 3 ;
xseq . n = (Bound2Lipschitz ((vseq . n),X)) . (0 * x) by A4, A11
.= 0 * ((Bound2Lipschitz ((vseq . n),X)) . x) by HAHNBAN:def 3 ;
hence |.((xseq . n) - (xseq . k)).| < e by A10, A12, COMPLEX1:44; :: thesis: verum

end;

end;

suppose x <> 0. X ; :: thesis: ex k being Nat st
for n being Nat st b₃ >= n holds
|.((xseq . b₃) - (xseq . n)).| < k

then A13: ||.x.|| <> 0 by NORMSP_0:def 5;
then consider k being Nat such that
X2: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e / ||.x.|| by A10, A2, RSSPACE3:8;
take k = k; :: thesis: for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
thus for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e :: thesis: verum

proof

let n be Nat; :: thesis: ( n >= k implies |.((xseq . n) - (xseq . k)).| < e )
assume n >= k ; :: thesis: |.((xseq . n) - (xseq . k)).| < e
then ||.((vseq . n) - (vseq . k)).|| < e / ||.x.|| by X2;
then A18: ||.((vseq . n) - (vseq . k)).|| * ||.x.|| < (e / ||.x.||) * ||.x.|| by A13, XREAL_1:68;
A19: (e / ||.x.||) * ||.x.|| = (e * (||.x.|| ")) * ||.x.|| by XCMPLX_0:def 9
.= e * ((||.x.|| ") * ||.x.||)
.= e * 1 by A13, XCMPLX_0:def 7 ;
|.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| * ||.x.|| by A6;
hence |.((xseq . n) - (xseq . k)).| < e by A18, A19, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

hence S₁[x,y] by A4, SEQ_4:41; :: thesis: verum

end;

consider f being Function of the carrier of X,REAL such that
A20: for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of the carrier of X,REAL ;

A21: now :: thesis: for x, y being VECTOR of X holds tseq . (x + y) = (tseq . x) + (tseq . y)

let x, y be VECTOR of X; :: thesis: tseq . (x + y) = (tseq . x) + (tseq . y)
consider xseq being sequence of REAL such that
A22: ( ( for n being Nat holds xseq . n = (Bound2Lipschitz ((vseq . n),X)) . x ) & xseq is convergent & tseq . x = lim xseq ) by A20;
consider zseq being sequence of REAL such that
A25: ( ( for n being Nat holds zseq . n = (Bound2Lipschitz ((vseq . n),X)) . (x + y) ) & zseq is convergent & tseq . (x + y) = lim zseq ) by A20;
consider yseq being sequence of REAL such that
A27: ( ( for n being Nat holds yseq . n = (Bound2Lipschitz ((vseq . n),X)) . y ) & yseq is convergent & tseq . y = lim yseq ) by A20;

now :: thesis: for n being Nat holds zseq . n = (xseq . n) + (yseq . n)

let n be Nat; :: thesis: zseq . n = (xseq . n) + (yseq . n)
thus zseq . n = (Bound2Lipschitz ((vseq . n),X)) . (x + y) by A25
.= ((Bound2Lipschitz ((vseq . n),X)) . x) + ((Bound2Lipschitz ((vseq . n),X)) . y) by HAHNBAN:def 2
.= (xseq . n) + ((Bound2Lipschitz ((vseq . n),X)) . y) by A22
.= (xseq . n) + (yseq . n) by A27 ; :: thesis: verum

end;

then zseq = xseq + yseq by SEQ_1:7;
hence tseq . (x + y) = (tseq . x) + (tseq . y) by A22, A27, A25, SEQ_2:6; :: thesis: verum

end;

now :: thesis: for x being VECTOR of X
for a being Real holds tseq . (a * x) = a * (tseq . x)

let x be VECTOR of X; :: thesis: for a being Real holds tseq . (a * x) = a * (tseq . x)
let a be Real; :: thesis: tseq . (a * x) = a * (tseq . x)
consider xseq being sequence of REAL such that
A30: ( ( for n being Nat holds xseq . n = (Bound2Lipschitz ((vseq . n),X)) . x ) & xseq is convergent & tseq . x = lim xseq ) by A20;
consider zseq being sequence of REAL such that
A33: ( ( for n being Nat holds zseq . n = (Bound2Lipschitz ((vseq . n),X)) . (a * x) ) & zseq is convergent & tseq . (a * x) = lim zseq ) by A20;

now :: thesis: for n being Nat holds zseq . n = a * (xseq . n)

let n be Nat; :: thesis: zseq . n = a * (xseq . n)
thus zseq . n = (Bound2Lipschitz ((vseq . n),X)) . (a * x) by A33
.= a * ((Bound2Lipschitz ((vseq . n),X)) . x) by HAHNBAN:def 3
.= a * (xseq . n) by A30 ; :: thesis: verum

end;

then zseq = a (#) xseq by SEQ_1:9;
hence tseq . (a * x) = a * (tseq . x) by A30, A33, SEQ_2:8; :: thesis: verum

end;

then reconsider tseq = tseq as linear-Functional of X by A21, HAHNBAN:def 2, HAHNBAN:def 3;

B40: now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e )
assume e > 0 ; :: thesis: ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e
then consider k being Nat such that
A36: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8;
take k = k; :: thesis: for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e

hereby :: thesis: verum

let m be Nat; :: thesis: ( m >= k implies |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e )
assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e
then A37: ||.((vseq . m) - (vseq . k)).|| < e by A36;
A38: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def 4;
|.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1:9;
hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e by A38, A37, XXREAL_0:2; :: thesis: verum

end;

end;

then A40: ||.vseq.|| is convergent by SEQ_4:41;
A41: tseq is Lipschitzian

proof

take lim ||.vseq.|| ; :: according to DUALSP01:def 9 :: thesis: ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds |.(tseq . x).| <= (lim ||.vseq.||) * ||.x.|| ) )

A42: now :: thesis: for x being VECTOR of X holds |.(tseq . x).| <= (lim ||.vseq.||) * ||.x.||

let x be VECTOR of X; :: thesis: |.(tseq . x).| <= (lim ||.vseq.||) * ||.x.||
consider xseq being sequence of REAL such that
A43: ( ( for n being Nat holds xseq . n = (Bound2Lipschitz ((vseq . n),X)) . x ) & xseq is convergent & tseq . x = lim xseq ) by A20;
A46: |.(tseq . x).| = lim |.xseq.| by A43, SEQ_4:14;
A49: for n being Nat holds |.xseq.| . n <= (||.x.|| (#) ||.vseq.||) . n

proof

let n be Nat; :: thesis: |.xseq.| . n <= (||.x.|| (#) ||.vseq.||) . n
A50: |.xseq.| . n = |.(xseq . n).| by SEQ_1:12;
A51: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;
A48: xseq . n = (Bound2Lipschitz ((vseq . n),X)) . x by A43;
vseq . n is Lipschitzian linear-Functional of X by Def9;
then |.(xseq . n).| <= ||.(vseq . n).|| * ||.x.|| by A48, Th29, Th32;
hence |.xseq.| . n <= (||.x.|| (#) ||.vseq.||) . n by A50, A51, SEQ_1:9; :: thesis: verum

end;

lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.|| by B40, SEQ_4:41, SEQ_2:8;
hence |.(tseq . x).| <= (lim ||.vseq.||) * ||.x.|| by A46, A49, A40, SEQ_2:18, A43; :: thesis: verum

end;

now :: thesis: for n being Nat holds ||.vseq.|| . n >= 0

let n be Nat; :: thesis: ||.vseq.|| . n >= 0
||.(vseq . n).|| >= 0 ;
hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum

end;

hence ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds |.(tseq . x).| <= (lim ||.vseq.||) * ||.x.|| ) ) by B40, SEQ_4:41, A42, SEQ_2:17; :: thesis: verum

end;

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.||

proof

let e be Real; :: thesis: ( e > 0 implies 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.|| )
assume e > 0 ; :: thesis: 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.||
then consider k being Nat such that
A55: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8;
take k ; :: thesis: for n being Nat st n >= k holds
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||

now :: thesis: for n being Nat st n >= k holds
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||

let n be Nat; :: thesis: ( n >= k implies for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.|| )
assume A56: n >= k ; :: thesis: for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||

now :: thesis: for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||

let x be VECTOR of X; :: thesis: |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||
consider xseq being sequence of REAL such that
A57: for n being Nat holds
( xseq . n = (Bound2Lipschitz ((vseq . n),X)) . x & xseq is convergent & tseq . x = lim xseq ) by A20;
A60: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||

proof

let m, k be Nat; :: thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian linear-Functional of X by Def9;
A61: ( xseq . k = (Bound2Lipschitz ((vseq . k),X)) . x & xseq . m = (Bound2Lipschitz ((vseq . m),X)) . x ) by A57;
( vseq . m is Lipschitzian linear-Functional of X & vseq . k is Lipschitzian linear-Functional of X ) by Def9;
then ( Bound2Lipschitz ((vseq . m),X) = vseq . m & Bound2Lipschitz ((vseq . k),X) = vseq . k ) by Th29;
then (xseq . m) - (xseq . k) = h1 . x by A61, Th40;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th32; :: thesis: verum

end;

A64: for m being Nat st m >= k holds
|.((xseq . n) - (xseq . m)).| <= e * ||.x.||

proof

let m be Nat; :: thesis: ( m >= k implies |.((xseq . n) - (xseq . m)).| <= e * ||.x.|| )
assume m >= k ; :: thesis: |.((xseq . n) - (xseq . m)).| <= e * ||.x.||
then ||.((vseq . n) - (vseq . m)).|| < e by A55, A56;
then A66: ||.((vseq . n) - (vseq . m)).|| * ||.x.|| <= e * ||.x.|| by XREAL_1:64;
|.((xseq . n) - (xseq . m)).| <= ||.((vseq . n) - (vseq . m)).|| * ||.x.|| by A60;
hence |.((xseq . n) - (xseq . m)).| <= e * ||.x.|| by A66, XXREAL_0:2; :: thesis: verum

end;

|.((xseq . n) - (tseq . x)).| <= e * ||.x.||

proof

deffunc H₁( Nat) -> object = |.((xseq . $1) - (xseq . n)).|;
consider rseq being Real_Sequence such that
A67: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();

now :: thesis: for x being object st x in NAT holds
rseq . x = |.(xseq - (xseq . n)).| . x

let x be object ; :: thesis: ( x in NAT implies rseq . x = |.(xseq - (xseq . n)).| . x )
assume x in NAT ; :: thesis: rseq . x = |.(xseq - (xseq . n)).| . x
then reconsider k = x as Nat ;
thus rseq . x = |.((xseq . k) - (xseq . n)).| by A67
.= |.((xseq - (xseq . n)) . k).| by Def14
.= |.(xseq - (xseq . n)).| . x by SEQ_1:12 ; :: thesis: verum

end;

then A68: rseq = |.(xseq - (xseq . n)).| ;
A69: xseq - (xseq . n) is convergent by A57, Th121;
lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A57, Th121;
then A70: lim rseq = |.((tseq . x) - (xseq . n)).| by A57, Th121, A68, SEQ_4:14;
for m being Nat st m >= k holds
rseq . m <= e * ||.x.||

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= e * ||.x.|| )
assume A71: m >= k ; :: thesis: rseq . m <= e * ||.x.||
rseq . m = |.((xseq . m) - (xseq . n)).| by A67
.= |.((xseq . n) - (xseq . m)).| by COMPLEX1:60 ;
hence rseq . m <= e * ||.x.|| by A64, A71; :: thesis: verum

end;

then lim rseq <= e * ||.x.|| by A69, A68, Lm3;
hence |.((xseq . n) - (tseq . x)).| <= e * ||.x.|| by A70, COMPLEX1:60; :: thesis: verum

end;

hence |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.|| by A57; :: thesis: verum

end;

hence for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.|| ; :: thesis: verum

end;

hence for n being Nat st n >= k holds
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.|| ; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume A73: e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
consider k being Nat such that
A74: for n being Nat st n >= k holds
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.|| by A54, A73;

now :: thesis: for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e

set g1 = tseq;
let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A75: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e
reconsider h1 = (vseq . n) - tv as Lipschitzian linear-Functional of X by Def9;
set f1 = Bound2Lipschitz ((vseq . n),X);

A76: now :: thesis: for t being VECTOR of X st ||.t.|| <= 1 holds
|.(h1 . t).| <= e

let t be VECTOR of X; :: thesis: ( ||.t.|| <= 1 implies |.(h1 . t).| <= e )
assume ||.t.|| <= 1 ; :: thesis: |.(h1 . t).| <= e
then A77: e * ||.t.|| <= e * 1 by A73, XREAL_1:64;
A78: |.(((Bound2Lipschitz ((vseq . n),X)) . t) - (tseq . t)).| <= e * ||.t.|| by A74, A75;
vseq . n is Lipschitzian linear-Functional of X by Def9;
then Bound2Lipschitz ((vseq . n),X) = vseq . n by Th29;
then |.(h1 . t).| = |.(((Bound2Lipschitz ((vseq . n),X)) . t) - (tseq . t)).| by Th40;
hence |.(h1 . t).| <= e by A78, A77, XXREAL_0:2; :: thesis: verum

end;

A79: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= e

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= e )
assume r in PreNorms h1 ; :: thesis: r <= e
then ex t being VECTOR of X st
( r = |.(h1 . t).| & ||.t.|| <= 1 ) ;
hence r <= e by A76; :: thesis: verum

end;

( ( for s being Real st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence ||.((vseq . n) - tv).|| <= e by A79, Th30; :: thesis: verum

end;

hence ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e ; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( e > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A81: e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
then consider m being Nat such that
A82: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A72;
take m ; :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
then ( ||.((vseq . n) - tv).|| <= e / 2 & e / 2 < e ) by A82, A81, XREAL_1:216;
hence ||.((vseq . n) - tv).|| < e by XXREAL_0:2; :: thesis: verum

end;

end;

hence vseq is convergent ; :: thesis: verum