let X be non empty set ; :: thesis: for Y being ComplexNormSpace st Y is complete holds

for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let Y be ComplexNormSpace; :: thesis: ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent )

assume A1: Y is complete ; :: thesis: for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let vseq be sequence of (C_NormSpace_of_BoundedFunctions (X,Y)); :: 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 Y st

( ( for n being Nat holds xseq . n = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq );

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

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

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

A18: tseq is bounded

ex k being Nat st

for n being Nat st n >= k holds

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

reconsider tv = tseq as Point of (C_NormSpace_of_BoundedFunctions (X,Y)) by Def5;

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

for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let Y be ComplexNormSpace; :: thesis: ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent )

assume A1: Y is complete ; :: thesis: for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let vseq be sequence of (C_NormSpace_of_BoundedFunctions (X,Y)); :: 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 = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq );

A3: for x being Element of X ex y being Element of Y st S

proof

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

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

consider xseq being sequence of Y such that

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

A5: for n being Nat holds xseq . n = H_{1}(n)
_{1}[x, lim xseq]

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

then xseq is convergent by A1;

hence S_{1}[x, lim xseq]
by A5; :: thesis: verum

end;deffunc H

consider xseq being sequence of Y such that

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

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

proof

take
lim xseq
; :: thesis: S
let n be Nat; :: thesis: xseq . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

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

end;n in NAT by ORDINAL1:def 12;

hence xseq . n = H

A6: 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)).||

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

vseq . k is bounded Function of X, the carrier of Y by Def5;

then A8: modetrans ((vseq . k),X,Y) = vseq . k by Th14;

reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;

vseq . m is bounded Function of X, the carrier of Y by Def5;

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

( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A4, A7;

then (xseq . m) - (xseq . k) = h1 . x by A9, A8, Th25;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; :: thesis: verum

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

vseq . k is bounded Function of X, the carrier of Y by Def5;

then A8: modetrans ((vseq . k),X,Y) = vseq . k by Th14;

reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;

vseq . m is bounded Function of X, the carrier of Y by Def5;

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

( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A4, A7;

then (xseq . m) - (xseq . k) = h1 . x by A9, A8, Th25;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; :: thesis: verum

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

ex k being Nat st

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

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

then
xseq is Cauchy_sequence_by_Norm
by CSSPACE3:8;ex k being Nat st

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

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

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

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

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

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

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

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

thus ex k being Nat st

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

||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum

end;for n, m being Nat st n >= k & m >= k holds

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

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

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

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

thus ex k being Nat st

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

||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum

proof

consider k being Nat such that

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

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

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

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

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

||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum

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

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

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

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

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

||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum

proof

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

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

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

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A6;

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

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

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

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A6;

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

then xseq is convergent by A1;

hence S

A13: for x being Element of X holds S

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

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 A17:
||.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 A2, 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 A2, 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 )

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

then A16: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A15, NORMSP_0:def 4;

( |.(||.(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 A16, XXREAL_0:2; :: thesis: verum

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

then A16: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A15, NORMSP_0:def 4;

( |.(||.(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 A16, XXREAL_0:2; :: thesis: verum

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

A18: tseq is bounded

proof

A24:
for e being Real st e > 0 holds
take
lim ||.vseq.||
; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) )

end;A19: now :: thesis: for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.||

let x be Element of X; :: thesis: ||.(tseq . x).|| <= lim ||.vseq.||

consider xseq being sequence of Y such that

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

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

A22: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).||

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

end;consider xseq being sequence of Y such that

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

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

A22: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).||

proof

A23:
for n being Nat holds ||.xseq.|| . n <= ||.vseq.|| . n
let m be Nat; :: thesis: ||.(xseq . m).|| <= ||.(vseq . m).||

( vseq . m is bounded Function of X, the carrier of Y & xseq . m = (modetrans ((vseq . m),X,Y)) . x ) by A20, Def5;

hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th14, Th17; :: thesis: verum

end;( vseq . m is bounded Function of X, the carrier of Y & xseq . m = (modetrans ((vseq . m),X,Y)) . x ) by A20, Def5;

hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th14, Th17; :: thesis: verum

proof

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

( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A22, NORMSP_0:def 4;

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

end;( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A22, NORMSP_0:def 4;

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

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

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

hence
( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) )
by A17, A19, SEQ_2:17; :: thesis: verumlet n be Nat; :: thesis: ||.vseq.|| . n >= 0

||.(vseq . n).|| >= 0 by CLVECT_1:105;

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

end;||.(vseq . n).|| >= 0 by CLVECT_1:105;

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 Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e

proof

reconsider tseq = tseq as bounded Function of X, the carrier of Y by A18;
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,Y)) . 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,Y)) . x) - (tseq . x)).|| <= e

then consider k being Nat such that

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

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

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

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

for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . 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,Y)) . 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,Y)) . x) - (tseq . x)).|| <= e

then consider k being Nat such that

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

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

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

for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . 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,Y)) . x) - (tseq . x)).|| <= e

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

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

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

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

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

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

consider xseq being sequence of Y such that

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

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

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

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

end;consider xseq being sequence of Y such that

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

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

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

proof

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

vseq . k is bounded Function of X, the carrier of Y by Def5;

then A30: modetrans ((vseq . k),X,Y) = vseq . k by Th14;

reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;

vseq . m is bounded Function of X, the carrier of Y by Def5;

then A31: modetrans ((vseq . m),X,Y) = vseq . m by Th14;

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

then (xseq . m) - (xseq . k) = h1 . x by A31, A30, Th25;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; :: thesis: verum

end;vseq . k is bounded Function of X, the carrier of Y by Def5;

then A30: modetrans ((vseq . k),X,Y) = vseq . k by Th14;

reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;

vseq . m is bounded Function of X, the carrier of Y by Def5;

then A31: modetrans ((vseq . m),X,Y) = vseq . m by Th14;

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

then (xseq . m) - (xseq . k) = h1 . x by A31, A30, Th25;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; :: thesis: verum

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

proof

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

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

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

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A29;

hence ||.((xseq . n) - (xseq . m)).|| <= e by A33, XXREAL_0:2; :: thesis: verum

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

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

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A29;

hence ||.((xseq . n) - (xseq . m)).|| <= e by A33, XXREAL_0:2; :: thesis: verum

proof

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

consider rseq being Real_Sequence such that

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

A36: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A28, CLVECT_1:115, CLVECT_1:121;

then A37: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A35, CLOPBAN1:19;

for m being Nat st m >= k holds

rseq . m <= e

hence ||.((xseq . n) - (tseq . x)).|| <= e by A37, CLVECT_1:108; :: thesis: verum

end;consider rseq being Real_Sequence such that

A34: 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 A35:
rseq = ||.(xseq - (xseq . n)).||
by FUNCT_2:12;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 A34

.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4

.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def 4 ; :: 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 A34

.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4

.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def 4 ; :: thesis: verum

A36: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A28, CLVECT_1:115, CLVECT_1:121;

then A37: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A35, CLOPBAN1:19;

for m being Nat st m >= k holds

rseq . m <= e

proof

then
lim rseq <= e
by A36, A35, Lm12, CLOPBAN1:19;
let m be Nat; :: thesis: ( m >= k implies rseq . m <= e )

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

rseq . m = ||.((xseq . m) - (xseq . n)).|| by A34

.= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1:108 ;

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

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

rseq . m = ||.((xseq . m) - (xseq . n)).|| by A34

.= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1:108 ;

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

hence ||.((xseq . n) - (tseq . x)).|| <= e by A37, CLVECT_1:108; :: thesis: verum

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

reconsider tv = tseq as Point of (C_NormSpace_of_BoundedFunctions (X,Y)) by Def5;

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

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

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

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

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

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

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 A41: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e

reconsider h1 = (vseq . n) - tv as bounded Function of X, the carrier of Y by Def5;

set f1 = modetrans ((vseq . n),X,Y);

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

(ComplexBoundedFunctionsNorm (X,Y)) . ((vseq . n) - tv) = upper_bound (PreNorms h1) by Th15;

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

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

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

reconsider h1 = (vseq . n) - tv as bounded Function of X, the carrier of Y by Def5;

set f1 = modetrans ((vseq . n),X,Y);

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

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

vseq . n is bounded Function of X, the carrier of Y by Def5;

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

then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th25;

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

end;vseq . n is bounded Function of X, the carrier of Y by Def5;

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

then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th25;

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

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

r <= e

A44:
( ( 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 A42; :: 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 A42; :: thesis: verum

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

(ComplexBoundedFunctionsNorm (X,Y)) . ((vseq . n) - tv) = upper_bound (PreNorms h1) by Th15;

hence ||.((vseq . n) - tv).|| <= e by A43, A44; :: 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
by CLVECT_1:def 15; :: 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 A45: e > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

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

reconsider ee = e as Real ;

consider m being Nat such that

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

||.((vseq . n) - tv).|| <= ee / 2 by A39, A45;

A47: e / 2 < e by A45, XREAL_1:216;

for n being Nat st n >= m holds

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

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

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

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

for n being Nat st n >= m holds

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

reconsider ee = e as Real ;

consider m being Nat such that

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

||.((vseq . n) - tv).|| <= ee / 2 by A39, A45;

A47: e / 2 < e by A45, XREAL_1:216;

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

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

hence
ex m being Nat st ||.((vseq . n) - tv).|| < e

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

hence ||.((vseq . n) - tv).|| < e by A47, XXREAL_0:2; :: thesis: verum

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

then ||.((vseq . n) - tv).|| <= e / 2 by A46;

hence ||.((vseq . n) - tv).|| < e by A47, XXREAL_0:2; :: thesis: verum

for n being Nat st n >= m holds

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