let X be non empty set ; :: thesis: for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds

seq is convergent

let vseq be sequence of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( vseq is CCauchy implies vseq is convergent )

defpred S_{1}[ set , set ] means ex xseq being Complex_Sequence st

for n being Nat holds

( xseq . n = (modetrans ((vseq . n),X)) . $1 & xseq is convergent & $2 = lim xseq );

assume A1: vseq is CCauchy ; :: thesis: vseq is convergent

A2: for x being Element of X ex y being Element of COMPLEX st S_{1}[x,y]

A13: for x being Element of X holds S_{1}[x,tseq . x]
from FUNCT_2:sch 3(A2);

|.(tseq /. x).| <= lim ||.vseq.|| ;

then tseq | X is bounded by CFUNCT_1:69;

then tseq in ComplexBoundedFunctions X ;

then reconsider tv = tseq as Point of (C_Normed_Algebra_of_BoundedFunctions X) ;

A25: for e being Real st e > 0 holds

ex k being Nat st

for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

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 (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( vseq is CCauchy implies vseq is convergent )

defpred S

for n being Nat holds

( xseq . n = (modetrans ((vseq . n),X)) . $1 & xseq is convergent & $2 = lim xseq );

assume A1: vseq is CCauchy ; :: thesis: vseq is convergent

A2: for x being Element of X ex y being Element of COMPLEX st S

proof

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

deffunc H_{1}( Nat) -> Element of COMPLEX = (modetrans ((vseq . $1),X)) . x;

consider xseq being Complex_Sequence such that

A3: for n being Element of NAT holds xseq . n = H_{1}(n)
from FUNCT_2:sch 4();

A4: for n being Nat holds xseq . n = H_{1}(n)

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

A5: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

hence S_{1}[x,y]
by A4; :: thesis: verum

end;deffunc H

consider xseq being Complex_Sequence such that

A3: for n being Element of NAT holds xseq . n = H

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

proof

reconsider y = lim xseq as Element of COMPLEX by XCMPLX_0:def 2;
let n be Nat; :: thesis: xseq . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence xseq . n = H_{1}(n)
by A3; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence xseq . n = H

take y ; :: thesis: S

A5: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Nat; :: thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

A6: ( m in NAT & k in NAT ) by ORDINAL1:def 12;

(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A7: h1 = (vseq . m) - (vseq . k) and

A8: h1 | X is bounded ;

vseq . m in ComplexBoundedFunctions X ;

then ex vseqm being Function of X,COMPLEX st

( vseq . m = vseqm & vseqm | X is bounded ) ;

then A9: modetrans ((vseq . m),X) = vseq . m by Th12;

vseq . k in ComplexBoundedFunctions X ;

then ex vseqk being Function of X,COMPLEX st

( vseq . k = vseqk & vseqk | X is bounded ) ;

then A10: modetrans ((vseq . k),X) = vseq . k by Th12;

( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A3, A6;

then (xseq . m) - (xseq . k) = h1 . x by A9, A10, A7, Th26;

hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A7, A8, Th19; :: thesis: verum

end;A6: ( m in NAT & k in NAT ) by ORDINAL1:def 12;

(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A7: h1 = (vseq . m) - (vseq . k) and

A8: h1 | X is bounded ;

vseq . m in ComplexBoundedFunctions X ;

then ex vseqm being Function of X,COMPLEX st

( vseq . m = vseqm & vseqm | X is bounded ) ;

then A9: modetrans ((vseq . m),X) = vseq . m by Th12;

vseq . k in ComplexBoundedFunctions X ;

then ex vseqk being Function of X,COMPLEX st

( vseq . k = vseqk & vseqk | X is bounded ) ;

then A10: modetrans ((vseq . k),X) = vseq . k by Th12;

( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A3, A6;

then (xseq . m) - (xseq . k) = h1 . x by A9, A10, A7, Th26;

hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A7, A8, Th19; :: 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

then
xseq is convergent
by COMSEQ_3:46;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 n >= k holds

|.((xseq . n) - (xseq . k)).| < e )

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

for n being Nat st n >= k holds

|.((xseq . n) - (xseq . k)).| < e

then consider k being Nat such that

A11: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;

reconsider k = k as Nat ;

take k = k; :: thesis: for n being Nat st n >= k holds

|.((xseq . n) - (xseq . k)).| < e

end;for n being Nat st n >= k holds

|.((xseq . n) - (xseq . k)).| < e )

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

for n being Nat st n >= k holds

|.((xseq . n) - (xseq . k)).| < e

then consider k being Nat such that

A11: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;

reconsider k = k as Nat ;

take k = k; :: thesis: for n being Nat st n >= k holds

|.((xseq . n) - (xseq . k)).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= k implies |.((xseq . n) - (xseq . k)).| < e )

assume n >= k ; :: thesis: |.((xseq . n) - (xseq . k)).| < e

then A12: ||.((vseq . n) - (vseq . k)).|| < e by A11;

|.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| by A5;

hence |.((xseq . n) - (xseq . k)).| < e by A12, XXREAL_0:2; :: thesis: verum

end;assume n >= k ; :: thesis: |.((xseq . n) - (xseq . k)).| < e

then A12: ||.((vseq . n) - (vseq . k)).|| < e by A11;

|.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| by A5;

hence |.((xseq . n) - (xseq . k)).| < e by A12, XXREAL_0:2; :: thesis: verum

hence S

A13: for x being Element of X holds S

now :: thesis: for e1 being Real st e1 > 0 holds

ex k being Nat st

for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

then A18:
||.vseq.|| is convergent
by SEQ_4:41;ex k being Nat st

for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Nat st

for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )

assume A14: e1 > 0 ; :: thesis: ex k being Nat st

for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

reconsider e = e1 as Real ;

consider k being Nat such that

A15: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, A14, CSSPACE3:8;

take k = k; :: thesis: for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum

end;for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )

assume A14: e1 > 0 ; :: thesis: ex k being Nat st

for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

reconsider e = e1 as Real ;

consider k being Nat such that

A15: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, A14, CSSPACE3:8;

take k = k; :: thesis: for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

now :: thesis: for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

hence
for m being Nat st m >= k holds |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

let m be Nat; :: thesis: ( m >= k implies |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )

A16: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;

assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

then A17: ||.((vseq . m) - (vseq . k)).|| < e by A15;

( |.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by CLVECT_1:110, NORMSP_0:def 4;

hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A17, A16, XXREAL_0:2; :: thesis: verum

end;A16: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;

assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

then A17: ||.((vseq . m) - (vseq . k)).|| < e by A15;

( |.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by CLVECT_1:110, NORMSP_0:def 4;

hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A17, A16, XXREAL_0:2; :: thesis: verum

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum

now :: thesis: for x being set st x in X /\ (dom tseq) holds

|.(tseq . x).| <= lim ||.vseq.||

then
for x being Element of X st x in X /\ (dom tseq) holds |.(tseq . x).| <= lim ||.vseq.||

let x be set ; :: thesis: ( x in X /\ (dom tseq) implies |.(tseq . x).| <= lim ||.vseq.|| )

assume A19: x in X /\ (dom tseq) ; :: thesis: |.(tseq . x).| <= lim ||.vseq.||

then consider xseq being Complex_Sequence such that

A20: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and

A21: ( xseq is convergent & tseq . x = lim xseq ) by A13;

A22: for n being Nat holds |.xseq.| . n <= ||.vseq.|| . n

hence |.(tseq . x).| <= lim ||.vseq.|| by A18, A22, SEQ_2:18; :: thesis: verum

end;assume A19: x in X /\ (dom tseq) ; :: thesis: |.(tseq . x).| <= lim ||.vseq.||

then consider xseq being Complex_Sequence such that

A20: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and

A21: ( xseq is convergent & tseq . x = lim xseq ) by A13;

A22: for n being Nat holds |.xseq.| . n <= ||.vseq.|| . n

proof

( |.xseq.| is convergent & |.(tseq . x).| = lim |.xseq.| )
by A21, SEQ_2:27;
let n be Nat; :: thesis: |.xseq.| . n <= ||.vseq.|| . n

A23: xseq . n = (modetrans ((vseq . n),X)) . x by A20;

vseq . n in ComplexBoundedFunctions X ;

then A24: ex h1 being Function of X,COMPLEX st

( vseq . n = h1 & h1 | X is bounded ) ;

then modetrans ((vseq . n),X) = vseq . n by Th12;

then |.(xseq . n).| <= ||.(vseq . n).|| by A19, A24, A23, Th19;

then |.xseq.| . n <= ||.(vseq . n).|| by VALUED_1:18;

hence |.xseq.| . n <= ||.vseq.|| . n by NORMSP_0:def 4; :: thesis: verum

end;A23: xseq . n = (modetrans ((vseq . n),X)) . x by A20;

vseq . n in ComplexBoundedFunctions X ;

then A24: ex h1 being Function of X,COMPLEX st

( vseq . n = h1 & h1 | X is bounded ) ;

then modetrans ((vseq . n),X) = vseq . n by Th12;

then |.(xseq . n).| <= ||.(vseq . n).|| by A19, A24, A23, Th19;

then |.xseq.| . n <= ||.(vseq . n).|| by VALUED_1:18;

hence |.xseq.| . n <= ||.vseq.|| . n by NORMSP_0:def 4; :: thesis: verum

hence |.(tseq . x).| <= lim ||.vseq.|| by A18, A22, SEQ_2:18; :: thesis: verum

|.(tseq /. x).| <= lim ||.vseq.|| ;

then tseq | X is bounded by CFUNCT_1:69;

then tseq in ComplexBoundedFunctions X ;

then reconsider tv = tseq as Point of (C_Normed_Algebra_of_BoundedFunctions X) ;

A25: for e being Real st e > 0 holds

ex k being Nat st

for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

proof

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

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )

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

for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

then consider k being Nat such that

A26: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;

take k ; :: thesis: for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

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

end;for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )

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

for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

then consider k being Nat such that

A26: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:8;

take k ; :: thesis: for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

now :: thesis: for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

hence
for n being Nat st n >= k holds for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

let n be Nat; :: thesis: ( n >= k implies for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )

assume A27: n >= k ; :: thesis: for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

end;assume A27: n >= k ; :: thesis: for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

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

hence
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
; :: thesis: verumlet x be Element of X; :: thesis: |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

consider xseq being Complex_Sequence such that

A28: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and

A29: xseq is convergent and

A30: tseq . x = lim xseq by A13;

reconsider xn = xseq . n as Element of COMPLEX by XCMPLX_0:def 2;

reconsider fseq = NAT --> xn as Complex_Sequence ;

set wseq = xseq - fseq;

deffunc H_{1}( Nat) -> object = |.((xseq . $1) - (xseq . n)).|;

consider rseq being Real_Sequence such that

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

A32: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

rseq . m <= e

A41: fseq is convergent by CFCONT_1:26;

A42: lim rseq <= e by A41, A37, A40, A29, RSSPACE2:5;

lim fseq = fseq . 0 by CFCONT_1:28;

then lim fseq = xseq . n ;

then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A29, A30, A41, COMSEQ_2:26;

then lim rseq = |.((tseq . x) - (xseq . n)).| by A41, A29, A40, SEQ_2:27;

then |.((xseq . n) - (tseq . x)).| <= e by A42, COMPLEX1:60;

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

end;consider xseq being Complex_Sequence such that

A28: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and

A29: xseq is convergent and

A30: tseq . x = lim xseq by A13;

reconsider xn = xseq . n as Element of COMPLEX by XCMPLX_0:def 2;

reconsider fseq = NAT --> xn as Complex_Sequence ;

set wseq = xseq - fseq;

deffunc H

consider rseq being Real_Sequence such that

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

A32: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

proof

A37:
for m being Nat st m >= k holds
let m, k be Nat; :: thesis: |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A33: h1 = (vseq . m) - (vseq . k) and

A34: h1 | X is bounded ;

vseq . m in ComplexBoundedFunctions X ;

then ex vseqm being Function of X,COMPLEX st

( vseq . m = vseqm & vseqm | X is bounded ) ;

then A35: modetrans ((vseq . m),X) = vseq . m by Th12;

vseq . k in ComplexBoundedFunctions X ;

then ex vseqk being Function of X,COMPLEX st

( vseq . k = vseqk & vseqk | X is bounded ) ;

then A36: modetrans ((vseq . k),X) = vseq . k by Th12;

( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A28;

then (xseq . m) - (xseq . k) = h1 . x by A35, A36, A33, Th26;

hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A33, A34, Th19; :: thesis: verum

end;(vseq . m) - (vseq . k) in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A33: h1 = (vseq . m) - (vseq . k) and

A34: h1 | X is bounded ;

vseq . m in ComplexBoundedFunctions X ;

then ex vseqm being Function of X,COMPLEX st

( vseq . m = vseqm & vseqm | X is bounded ) ;

then A35: modetrans ((vseq . m),X) = vseq . m by Th12;

vseq . k in ComplexBoundedFunctions X ;

then ex vseqk being Function of X,COMPLEX st

( vseq . k = vseqk & vseqk | X is bounded ) ;

then A36: modetrans ((vseq . k),X) = vseq . k by Th12;

( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A28;

then (xseq . m) - (xseq . k) = h1 . x by A35, A36, A33, Th26;

hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A33, A34, Th19; :: thesis: verum

rseq . m <= e

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= e )

assume m >= k ; :: thesis: rseq . m <= e

then A38: ||.((vseq . n) - (vseq . m)).|| < e by A26, A27;

rseq . m = |.((xseq . m) - (xseq . n)).| by A31;

then rseq . m = |.((xseq . n) - (xseq . m)).| by COMPLEX1:60;

then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A32;

hence rseq . m <= e by A38, XXREAL_0:2; :: thesis: verum

end;assume m >= k ; :: thesis: rseq . m <= e

then A38: ||.((vseq . n) - (vseq . m)).|| < e by A26, A27;

rseq . m = |.((xseq . m) - (xseq . n)).| by A31;

then rseq . m = |.((xseq . n) - (xseq . m)).| by COMPLEX1:60;

then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A32;

hence rseq . m <= e by A38, XXREAL_0:2; :: thesis: verum

A39: now :: thesis: for m being Element of NAT holds (xseq - fseq) . m = (xseq . m) - (xseq . n)

let m be Element of NAT ; :: thesis: (xseq - fseq) . m = (xseq . m) - (xseq . n)

(xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by VALUED_1:1

.= (xseq . m) - (fseq . m) by VALUED_1:8 ;

hence (xseq - fseq) . m = (xseq . m) - (xseq . n) ; :: thesis: verum

end;(xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by VALUED_1:1

.= (xseq . m) - (fseq . m) by VALUED_1:8 ;

hence (xseq - fseq) . m = (xseq . m) - (xseq . n) ; :: thesis: verum

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

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

then A40:
rseq = |.(xseq - fseq).|
by FUNCT_2:12;rseq . x = |.(xseq - fseq).| . x

let x be object ; :: thesis: ( x in NAT implies rseq . x = |.(xseq - fseq).| . x )

assume x in NAT ; :: thesis: rseq . x = |.(xseq - fseq).| . x

then reconsider k = x as Element of NAT ;

rseq . x = |.((xseq . k) - (xseq . n)).| by A31;

then rseq . x = |.((xseq - fseq) . k).| by A39;

hence rseq . x = |.(xseq - fseq).| . x by VALUED_1:18; :: thesis: verum

end;assume x in NAT ; :: thesis: rseq . x = |.(xseq - fseq).| . x

then reconsider k = x as Element of NAT ;

rseq . x = |.((xseq . k) - (xseq . n)).| by A31;

then rseq . x = |.((xseq - fseq) . k).| by A39;

hence rseq . x = |.(xseq - fseq).| . x by VALUED_1:18; :: thesis: verum

A41: fseq is convergent by CFCONT_1:26;

A42: lim rseq <= e by A41, A37, A40, A29, RSSPACE2:5;

lim fseq = fseq . 0 by CFCONT_1:28;

then lim fseq = xseq . n ;

then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A29, A30, A41, COMSEQ_2:26;

then lim rseq = |.((tseq . x) - (xseq . n)).| by A41, A29, A40, SEQ_2:27;

then |.((xseq . n) - (tseq . x)).| <= e by A42, COMPLEX1:60;

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

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

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 e > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

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

then consider k being Nat such that

A44: for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A25;

take k ; :: thesis: for n being Nat st n >= k holds

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

end;for n being Nat st n >= k holds

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

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

for n being Nat st n >= k holds

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

then consider k being Nat such that

A44: for n being Nat st n >= k holds

for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A25;

take k ; :: thesis: for n being Nat st n >= k holds

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

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )

assume A45: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e

vseq . n in ComplexBoundedFunctions X ;

then consider f1 being Function of X,COMPLEX such that

A46: f1 = vseq . n and

f1 | X is bounded ;

(vseq . n) - tv in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A47: h1 = (vseq . n) - tv and

A48: h1 | X is bounded ;

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

hence ||.((vseq . n) - tv).|| <= e by A47, A48, A50, Th13; :: thesis: verum

end;assume A45: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e

vseq . n in ComplexBoundedFunctions X ;

then consider f1 being Function of X,COMPLEX such that

A46: f1 = vseq . n and

f1 | X is bounded ;

(vseq . n) - tv in ComplexBoundedFunctions X ;

then consider h1 being Function of X,COMPLEX such that

A47: h1 = (vseq . n) - tv and

A48: h1 | X is bounded ;

A49: now :: thesis: for t being Element of X holds |.(h1 . t).| <= e

let t be Element of X; :: thesis: |.(h1 . t).| <= e

( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A46, A47, Def7, Th26;

hence |.(h1 . t).| <= e by A44, A45; :: thesis: verum

end;( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A46, A47, Def7, Th26;

hence |.(h1 . t).| <= e by A44, A45; :: thesis: verum

A50: 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 Element of X st r = |.(h1 . t).| ;

hence r <= e by A49; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= e

then ex t being Element of X st r = |.(h1 . t).| ;

hence r <= e by A49; :: thesis: verum

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

hence ||.((vseq . n) - tv).|| <= e by A47, A48, A50, Th13; :: 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 A51: e > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

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

consider m being Nat such that

A52: for n being Nat st n >= m holds

||.((vseq . n) - tv).|| <= e / 2 by A43, A51;

take m ; :: thesis: for n being Nat st n >= m holds

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

A53: e / 2 < e by A51, XREAL_1:216;

end;for n being Nat st n >= m holds

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

assume A51: e > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

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

consider m being Nat such that

A52: for n being Nat st n >= m holds

||.((vseq . n) - tv).|| <= e / 2 by A43, A51;

take m ; :: thesis: for n being Nat st n >= m holds

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

A53: e / 2 < e by A51, XREAL_1:216;