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_{1}[ 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_{1}[x,y]

A20: for x being Element of X holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A3);

reconsider tseq = f as Function of the carrier of X,REAL ;

A41: tseq is Lipschitzian

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

ex m being Nat st

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e

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

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

proof

consider f being Function of the carrier of X,REAL such that
let x be Element of X; :: thesis: ex y being Element of REAL st S_{1}[x,y]

deffunc H_{1}( 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_{1}(n)
from SEQ_1:sch 1();

reconsider y = lim xseq as Element of REAL by XREAL_0:def 1;

take y ; :: thesis: S_{1}[x,y]

A6: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||_{1}[x,y]
by A4, SEQ_4:41; :: thesis: verum

end;deffunc H

consider xseq being Real_Sequence such that

A4: for n being Nat holds xseq . n = H

reconsider y = lim xseq as Element of REAL by XREAL_0:def 1;

take y ; :: thesis: S

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

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

hence
Sex 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_{3} >= n holds

|.((xseq . b_{3}) - (xseq . n)).| < k )

assume A10: e > 0 ; :: thesis: ex k being Nat st

for n being Nat st b_{3} >= n holds

|.((xseq . b_{3}) - (xseq . n)).| < k

end;for n being Nat st b

|.((xseq . b

assume A10: e > 0 ; :: thesis: ex k being Nat st

for n being Nat st b

|.((xseq . b

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

end;

suppose A11:
x = 0. X
; :: thesis: ex k being Nat st

for n being Nat st b_{3} >= n holds

|.((xseq . b_{3}) - (xseq . n)).| < k

for n being Nat st b

|.((xseq . b

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

end;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;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

suppose
x <> 0. X
; :: thesis: ex k being Nat st

for n being Nat st b_{3} >= n holds

|.((xseq . b_{3}) - (xseq . n)).| < k

for n being Nat st b

|.((xseq . b

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

end;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;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

A20: for x being Element of X holds S

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;

hence tseq . (x + y) = (tseq . x) + (tseq . y) by A22, A27, A25, SEQ_2:6; :: thesis: verum

end;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)

then
zseq = xseq + yseq
by SEQ_1:7;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;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

hence tseq . (x + y) = (tseq . x) + (tseq . y) by A22, A27, A25, SEQ_2:6; :: thesis: verum

now :: thesis: for x being VECTOR of X

for a being Real holds tseq . (a * x) = a * (tseq . x)

then reconsider tseq = tseq as linear-Functional of X by A21, HAHNBAN:def 2, HAHNBAN:def 3;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;

hence tseq . (a * x) = a * (tseq . x) by A30, A33, SEQ_2:8; :: thesis: verum

end;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)

then
zseq = a (#) xseq
by SEQ_1:9;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;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

hence tseq . (a * x) = a * (tseq . x) by A30, A33, SEQ_2:8; :: thesis: verum

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

then A40:
||.vseq.|| is convergent
by SEQ_4:41;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

end;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;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

A41: tseq is Lipschitzian

proof

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

end;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

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

end;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

lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.||
by B40, SEQ_4:41, SEQ_2:8;
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;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

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

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

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: verumlet n be Nat; :: thesis: ||.vseq.|| . n >= 0

||.(vseq . n).|| >= 0 ;

hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum

end;||.(vseq . n).|| >= 0 ;

hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum

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

reconsider tseq = tseq as Lipschitzian linear-Functional of X by A41;
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.||

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

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

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

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

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

hence
for x being VECTOR of X holds |.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||
; :: thesis: verumlet 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.||

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

end;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

A64:
for m being Nat st m >= k holds
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;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

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

proof

|.((xseq . n) - (tseq . x)).| <= e * ||.x.||
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;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

proof

hence
|.(((Bound2Lipschitz ((vseq . n),X)) . x) - (tseq . x)).| <= e * ||.x.||
by A57; :: thesis: verum
deffunc H_{1}( Nat) -> object = |.((xseq . $1) - (xseq . n)).|;

consider rseq being Real_Sequence such that

A67: for m being Nat holds rseq . m = H_{1}(m)
from SEQ_1:sch 1();

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

hence |.((xseq . n) - (tseq . x)).| <= e * ||.x.|| by A70, COMPLEX1:60; :: thesis: verum

end;consider rseq being Real_Sequence such that

A67: for m being Nat holds rseq . m = H

now :: thesis: for x being object st x in NAT holds

rseq . x = |.(xseq - (xseq . n)).| . x

then A68:
rseq = |.(xseq - (xseq . n)).|
;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;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

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

then
lim rseq <= e * ||.x.||
by A69, A68, Lm3;
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;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

hence |.((xseq . n) - (tseq . x)).| <= e * ||.x.|| by A70, COMPLEX1:60; :: thesis: verum

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

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

for e being Real st e > 0 holds
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;

for n being Nat st n >= k holds

||.((vseq . n) - tv).|| <= e ; :: thesis: verum

end;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

hence
ex k being Nat st ||.((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);

s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;

hence ||.((vseq . n) - tv).|| <= e by A79, Th30; :: thesis: verum

end;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

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

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

r <= e

( ( for s being Real st s 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;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

s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;

hence ||.((vseq . n) - tv).|| <= e by A79, Th30; :: thesis: verum

for n being Nat st n >= k holds

||.((vseq . n) - tv).|| <= e ; :: thesis: verum

ex m being Nat st

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e

proof

hence
vseq is convergent
; :: thesis: verum
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

end;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