let X, Y be ComplexNormSpace; :: thesis: ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (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_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let vseq be sequence of (C_NormSpace_of_BoundedLinearOperators (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]

A24: 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,Y ;

A45: tseq is Lipschitzian

ex k being Nat st

for n being Nat st n >= k holds

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

reconsider tv = tseq as Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) by Def7;

A76: 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 )

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

seq is convergent

let vseq be sequence of (C_NormSpace_of_BoundedLinearOperators (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 the carrier 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)).|| * ||.x.||

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)).|| * ||.x.||

proof

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

A7: k in NAT by ORDINAL1:def 12;

A8: m in NAT by ORDINAL1:def 12;

reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian LinearOperator of X,Y by Def7;

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

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

then A10: modetrans ((vseq . m),X,Y) = vseq . m by Th28;

vseq . k is Lipschitzian LinearOperator of X,Y by Def7;

then A11: modetrans ((vseq . k),X,Y) = vseq . k by Th28;

xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4, A8;

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

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

end;A7: k in NAT by ORDINAL1:def 12;

A8: m in NAT by ORDINAL1:def 12;

reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian LinearOperator of X,Y by Def7;

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

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

then A10: modetrans ((vseq . m),X,Y) = vseq . m by Th28;

vseq . k is Lipschitzian LinearOperator of X,Y by Def7;

then A11: modetrans ((vseq . k),X,Y) = vseq . k by Th28;

xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4, A8;

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

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th31; :: 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 A12: e > 0 ; :: thesis: ex k being Nat st

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

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

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

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

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

now :: thesis: ( ( x = 0. X & ex k being Element of NAT st

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

||.((xseq . n) - (xseq . m)).|| < e ) or ( x <> 0. X & ex k being Nat st

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

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

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

||.((xseq . n) - (xseq . m)).|| < e ) or ( x <> 0. X & ex k being Nat st

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

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

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

end;

case A13:
x = 0. X
; :: thesis: ex k being Element of NAT st

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

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

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

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

take k = 0 ; :: 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;||.((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 that

n >= k and

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

A14: n in NAT by ORDINAL1:def 12;

A15: m in NAT by ORDINAL1:def 12;

A16: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4, A15

.= (modetrans ((vseq . m),X,Y)) . (0c * x) by A13, CLVECT_1:1

.= 0c * ((modetrans ((vseq . m),X,Y)) . x) by Def3

.= 0. Y by CLVECT_1:1 ;

xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4, A14

.= (modetrans ((vseq . n),X,Y)) . (0c * x) by A13, CLVECT_1:1

.= 0c * ((modetrans ((vseq . n),X,Y)) . x) by Def3

.= 0. Y by CLVECT_1:1 ;

then ||.((xseq . n) - (xseq . m)).|| = ||.(0. Y).|| by A16, RLVECT_1:13

.= 0 by NORMSP_0:def 6 ;

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

end;assume that

n >= k and

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

A14: n in NAT by ORDINAL1:def 12;

A15: m in NAT by ORDINAL1:def 12;

A16: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4, A15

.= (modetrans ((vseq . m),X,Y)) . (0c * x) by A13, CLVECT_1:1

.= 0c * ((modetrans ((vseq . m),X,Y)) . x) by Def3

.= 0. Y by CLVECT_1:1 ;

xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4, A14

.= (modetrans ((vseq . n),X,Y)) . (0c * x) by A13, CLVECT_1:1

.= 0c * ((modetrans ((vseq . n),X,Y)) . x) by Def3

.= 0. Y by CLVECT_1:1 ;

then ||.((xseq . n) - (xseq . m)).|| = ||.(0. Y).|| by A16, RLVECT_1:13

.= 0 by NORMSP_0:def 6 ;

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

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

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

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

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

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

then A17:
||.x.|| <> 0
by NORMSP_0:def 5;

then A18: ||.x.|| > 0 by CLVECT_1:105;

then consider k being Nat such that

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

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

take k = 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;then A18: ||.x.|| > 0 by CLVECT_1:105;

then consider k being Nat such that

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

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

take k = 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 that

A20: n >= k and

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

||.((vseq . n) - (vseq . m)).|| < e / ||.x.|| by A19, A20, A21;

then A22: ||.((vseq . n) - (vseq . m)).|| * ||.x.|| < (e / ||.x.||) * ||.x.|| by A18, XREAL_1:68;

A23: (e / ||.x.||) * ||.x.|| = (e * (||.x.|| ")) * ||.x.|| by XCMPLX_0:def 9

.= e * ((||.x.|| ") * ||.x.||)

.= e * 1 by A17, XCMPLX_0:def 7

.= e ;

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

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

end;assume that

A20: n >= k and

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

||.((vseq . n) - (vseq . m)).|| < e / ||.x.|| by A19, A20, A21;

then A22: ||.((vseq . n) - (vseq . m)).|| * ||.x.|| < (e / ||.x.||) * ||.x.|| by A18, XREAL_1:68;

A23: (e / ||.x.||) * ||.x.|| = (e * (||.x.|| ")) * ||.x.|| by XCMPLX_0:def 9

.= e * ((||.x.|| ") * ||.x.||)

.= e * 1 by A17, XCMPLX_0:def 7

.= e ;

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

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

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

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

then xseq is convergent by A1;

hence S

A24: for x being Element of X holds S

reconsider tseq = f as Function of X,Y ;

A25: 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 Y such that

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

A27: xseq is convergent and

A28: tseq . x = lim xseq by A24;

consider zseq being sequence of Y such that

A29: for n being Nat holds zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) and

zseq is convergent and

A30: tseq . (x + y) = lim zseq by A24;

consider yseq being sequence of Y such that

A31: for n being Nat holds yseq . n = (modetrans ((vseq . n),X,Y)) . y and

A32: yseq is convergent and

A33: tseq . y = lim yseq by A24;

hence tseq . (x + y) = (tseq . x) + (tseq . y) by A27, A28, A32, A33, A30, CLVECT_1:119; :: thesis: verum

end;consider xseq being sequence of Y such that

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

A27: xseq is convergent and

A28: tseq . x = lim xseq by A24;

consider zseq being sequence of Y such that

A29: for n being Nat holds zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) and

zseq is convergent and

A30: tseq . (x + y) = lim zseq by A24;

consider yseq being sequence of Y such that

A31: for n being Nat holds yseq . n = (modetrans ((vseq . n),X,Y)) . y and

A32: yseq is convergent and

A33: tseq . y = lim yseq by A24;

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

then
zseq = xseq + yseq
by NORMSP_1:def 2;let n be Nat; :: thesis: zseq . n = (xseq . n) + (yseq . n)

thus zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) by A29

.= ((modetrans ((vseq . n),X,Y)) . x) + ((modetrans ((vseq . n),X,Y)) . y) by VECTSP_1:def 20

.= (xseq . n) + ((modetrans ((vseq . n),X,Y)) . y) by A26

.= (xseq . n) + (yseq . n) by A31 ; :: thesis: verum

end;thus zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) by A29

.= ((modetrans ((vseq . n),X,Y)) . x) + ((modetrans ((vseq . n),X,Y)) . y) by VECTSP_1:def 20

.= (xseq . n) + ((modetrans ((vseq . n),X,Y)) . y) by A26

.= (xseq . n) + (yseq . n) by A31 ; :: thesis: verum

hence tseq . (x + y) = (tseq . x) + (tseq . y) by A27, A28, A32, A33, A30, CLVECT_1:119; :: thesis: verum

now :: thesis: for x being VECTOR of X

for c being Complex holds tseq . (c * x) = c * (tseq . x)

then reconsider tseq = tseq as LinearOperator of X,Y by A25, Def3, VECTSP_1:def 20;for c being Complex holds tseq . (c * x) = c * (tseq . x)

let x be VECTOR of X; :: thesis: for c being Complex holds tseq . (c * x) = c * (tseq . x)

let c be Complex; :: thesis: tseq . (c * x) = c * (tseq . x)

consider xseq being sequence of Y such that

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

A35: xseq is convergent and

A36: tseq . x = lim xseq by A24;

consider zseq being sequence of Y such that

A37: for n being Nat holds zseq . n = (modetrans ((vseq . n),X,Y)) . (c * x) and

zseq is convergent and

A38: tseq . (c * x) = lim zseq by A24;

hence tseq . (c * x) = c * (tseq . x) by A35, A36, A38, CLVECT_1:122; :: thesis: verum

end;let c be Complex; :: thesis: tseq . (c * x) = c * (tseq . x)

consider xseq being sequence of Y such that

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

A35: xseq is convergent and

A36: tseq . x = lim xseq by A24;

consider zseq being sequence of Y such that

A37: for n being Nat holds zseq . n = (modetrans ((vseq . n),X,Y)) . (c * x) and

zseq is convergent and

A38: tseq . (c * x) = lim zseq by A24;

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

then
zseq = c * xseq
by CLVECT_1:def 14;let n be Nat; :: thesis: zseq . n = c * (xseq . n)

thus zseq . n = (modetrans ((vseq . n),X,Y)) . (c * x) by A37

.= c * ((modetrans ((vseq . n),X,Y)) . x) by Def3

.= c * (xseq . n) by A34 ; :: thesis: verum

end;thus zseq . n = (modetrans ((vseq . n),X,Y)) . (c * x) by A37

.= c * ((modetrans ((vseq . n),X,Y)) . x) by Def3

.= c * (xseq . n) by A34 ; :: thesis: verum

hence tseq . (c * x) = c * (tseq . x) by A35, A36, A38, CLVECT_1:122; :: thesis: verum

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

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

||.((vseq . n) - (vseq . m)).|| < e by A2, A39, 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 A39: 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

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

||.((vseq . n) - (vseq . m)).|| < e by A2, A39, 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 A41: ||.((vseq . m) - (vseq . k)).|| < e by A40;

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

A43: ||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def 4;

|.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by CLVECT_1:110;

hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A43, A42, A41, XXREAL_0:2; :: thesis: verum

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

then A41: ||.((vseq . m) - (vseq . k)).|| < e by A40;

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

A43: ||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def 4;

|.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by CLVECT_1:110;

hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A43, A42, A41, XXREAL_0:2; :: thesis: verum

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

A45: tseq is Lipschitzian

proof

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

end;A46: 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 Y such that

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

A48: xseq is convergent and

A49: tseq . x = lim xseq by A24;

A50: ||.(tseq . x).|| = lim ||.xseq.|| by A48, A49, Th19;

A51: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||

A57: lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.|| by A44, SEQ_2:8;

||.xseq.|| is convergent by A48, A49, Th19;

hence ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| by A50, A53, A56, A57, SEQ_2:18; :: thesis: verum

end;consider xseq being sequence of Y such that

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

A48: xseq is convergent and

A49: tseq . x = lim xseq by A24;

A50: ||.(tseq . x).|| = lim ||.xseq.|| by A48, A49, Th19;

A51: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||

proof

A53:
for n being Nat holds ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
let m be Nat; :: thesis: ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||

A52: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A47;

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

hence ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.|| by A52, Th28, Th31; :: thesis: verum

end;A52: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A47;

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

hence ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.|| by A52, Th28, Th31; :: thesis: verum

proof

A56:
||.x.|| (#) ||.vseq.|| is convergent
by A44;
let n be Nat; :: thesis: ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n

A54: ||.xseq.|| . n = ||.(xseq . n).|| by NORMSP_0:def 4;

A55: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;

||.(xseq . n).|| <= ||.(vseq . n).|| * ||.x.|| by A51;

hence ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n by A54, A55, SEQ_1:9; :: thesis: verum

end;A54: ||.xseq.|| . n = ||.(xseq . n).|| by NORMSP_0:def 4;

A55: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;

||.(xseq . n).|| <= ||.(vseq . n).|| * ||.x.|| by A51;

hence ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n by A54, A55, SEQ_1:9; :: thesis: verum

A57: lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.|| by A44, SEQ_2:8;

||.xseq.|| is convergent by A48, A49, Th19;

hence ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| by A50, A53, A56, A57, SEQ_2:18; :: 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 A44, A46, 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 VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||

proof

reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A45;
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 ||.(((modetrans ((vseq . n),X,Y)) . 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 ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||

then consider k being Nat such that

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

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

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

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

then consider k being Nat such that

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

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

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

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

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

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

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

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

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

consider xseq being sequence of Y such that

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

A62: xseq is convergent and

A63: tseq . x = lim xseq by A24;

A64: 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 Y such that

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

A62: xseq is convergent and

A63: tseq . x = lim xseq by A24;

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

proof

A68:
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 LinearOperator of X,Y by Def7;

A65: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A61;

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

then A66: modetrans ((vseq . m),X,Y) = vseq . m by Th28;

vseq . k is Lipschitzian LinearOperator of X,Y by Def7;

then A67: modetrans ((vseq . k),X,Y) = vseq . k by Th28;

xseq . m = (modetrans ((vseq . m),X,Y)) . x by A61;

then (xseq . m) - (xseq . k) = h1 . x by A66, A67, A65, Th39;

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

end;reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian LinearOperator of X,Y by Def7;

A65: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A61;

vseq . m is Lipschitzian LinearOperator of X,Y by Def7;

then A66: modetrans ((vseq . m),X,Y) = vseq . m by Th28;

vseq . k is Lipschitzian LinearOperator of X,Y by Def7;

then A67: modetrans ((vseq . k),X,Y) = vseq . k by Th28;

xseq . m = (modetrans ((vseq . m),X,Y)) . x by A61;

then (xseq . m) - (xseq . k) = h1 . x by A66, A67, A65, Th39;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th31; :: 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 A69: ||.((vseq . n) - (vseq . m)).|| < e by A59, A60;

A70: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * ||.x.|| by A64;

0 <= ||.x.|| by CLVECT_1:105;

then ||.((vseq . n) - (vseq . m)).|| * ||.x.|| <= e * ||.x.|| by A69, XREAL_1:64;

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

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

then A69: ||.((vseq . n) - (vseq . m)).|| < e by A59, A60;

A70: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * ||.x.|| by A64;

0 <= ||.x.|| by CLVECT_1:105;

then ||.((vseq . n) - (vseq . m)).|| * ||.x.|| <= e * ||.x.|| by A69, XREAL_1:64;

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

proof

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

consider rseq being Real_Sequence such that

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

A73: xseq - (xseq . n) is convergent by A62, CLVECT_1:115;

lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A62, A63, CLVECT_1:121;

then A74: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A73, A72, Th40;

for m being Nat st m >= k holds

rseq . m <= e * ||.x.||

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

end;consider rseq being Real_Sequence such that

A71: 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 A72:
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 A71

.= ||.((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 A71

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

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

A73: xseq - (xseq . n) is convergent by A62, CLVECT_1:115;

lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A62, A63, CLVECT_1:121;

then A74: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A73, A72, Th40;

for m being Nat st m >= k holds

rseq . m <= e * ||.x.||

proof

then
lim rseq <= e * ||.x.||
by A73, A72, Lm2, Th40;
let m be Nat; :: thesis: ( m >= k implies rseq . m <= e * ||.x.|| )

assume A75: m >= k ; :: thesis: rseq . m <= e * ||.x.||

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

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

hence rseq . m <= e * ||.x.|| by A68, A75; :: thesis: verum

end;assume A75: m >= k ; :: thesis: rseq . m <= e * ||.x.||

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

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

hence rseq . m <= e * ||.x.|| by A68, A75; :: thesis: verum

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

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

reconsider tv = tseq as Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) by Def7;

A76: 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 A77: 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

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

for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| by A58, A77;

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

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

for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| by A58, A77;

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

reconsider h1 = (vseq . n) - tv as Lipschitzian LinearOperator of X,Y by Def7;

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

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

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

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

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

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

reconsider h1 = (vseq . n) - tv as Lipschitzian LinearOperator of X,Y by Def7;

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

A80: 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 A81: e * ||.t.|| <= e * 1 by A77, XREAL_1:64;

A82: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * ||.t.|| by A78, A79;

vseq . n is Lipschitzian LinearOperator of X,Y by Def7;

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

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

hence ||.(h1 . t).|| <= e by A82, A81, XXREAL_0:2; :: thesis: verum

end;assume ||.t.|| <= 1 ; :: thesis: ||.(h1 . t).|| <= e

then A81: e * ||.t.|| <= e * 1 by A77, XREAL_1:64;

A82: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * ||.t.|| by A78, A79;

vseq . n is Lipschitzian LinearOperator of X,Y by Def7;

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

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

hence ||.(h1 . t).|| <= e by A82, A81, XXREAL_0:2; :: thesis: verum

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

r <= e

A84:
( ( 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 A80; :: 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 A80; :: thesis: verum

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

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

hence ||.((vseq . n) - tv).|| <= e by A83, A84; :: 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 A85: 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

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

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

A87: e / 2 < e by A85, 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 A85: 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

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

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

A87: e / 2 < e by A85, 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 A86;

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

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

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

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

for n being Nat st n >= m holds

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