let X, Y be ComplexNormSpace; :: thesis:
assume A1: Y is complete ; :: thesis:
let vseq be sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis:
assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis:
defpred S₁[ 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₁[x,y]

let x be Element of X; :: thesis:
deffunc H₁( 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₁(n) from FUNCT_2:sch 4();
A5: for n being Nat holds xseq . n = H₁(n)

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence xseq . n = H₁(n) by A4; :: thesis:

end;

take lim xseq ; :: thesis:
A6: for m, k being Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||

proof

let m, k be Nat; :: thesis:
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:

end;

now :: thesis:

let e be Real; :: thesis:
assume A12: e > 0 ; :: thesis:

now :: thesis:

per cases ;

case A13: x = 0. X ; :: thesis:

take k = 0 ; :: thesis:
thus for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis:

proof

let n, m be Nat; :: thesis:
assume that
n >= k and
m >= k ; :: thesis:
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:

end;

case x <> 0. X ; :: thesis:

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:
thus for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis:

proof

let n, m be Nat; :: thesis:
assume that
A20: n >= k and
A21: m >= k ; :: thesis:
||.((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:

end;

hence ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ; :: thesis:

end;

then xseq is Cauchy_sequence_by_Norm by CSSPACE3:8;
then xseq is convergent by A1;
hence S₁[x, lim xseq] by A5; :: thesis:

end;

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

A25: now :: thesis:

let x, y be VECTOR of X; :: thesis:
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:

let n be Nat; :: thesis:
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:

end;

then zseq = xseq + yseq by NORMSP_1:def 2;
hence tseq . (x + y) = (tseq . x) + (tseq . y) by A27, A28, A32, A33, A30, CLVECT_1:119; :: thesis:

end;

now :: thesis:

let x be VECTOR of X; :: thesis:
let c be Complex; :: thesis:
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:

let n be Nat; :: thesis:
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:

end;

then zseq = c * xseq by CLVECT_1:def 14;
hence tseq . (c * x) = c * (tseq . x) by A35, A36, A38, CLVECT_1:122; :: thesis:

end;

then reconsider tseq = tseq as LinearOperator of X,Y by A25, Def3, VECTSP_1:def 20;

now :: thesis:

let e1 be Real; :: thesis:
assume A39: e1 > 0 ; :: thesis:
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:

now :: thesis:

let m be Nat; :: thesis:
assume m >= k ; :: thesis:
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:

end;

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

end;

then A44: ||.vseq.|| is convergent by SEQ_4:41;
A45: tseq is Lipschitzian

proof

take lim ||.vseq.|| ; :: according to CLOPBAN1:def 6 :: thesis:

A46: now :: thesis:

let x be VECTOR of X; :: thesis:
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

let m be Nat; :: thesis:
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:

end;

A53: for n being Nat holds ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n

proof

let n be Nat; :: thesis:
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:

end;

A56: ||.x.|| (#) ||.vseq.|| is convergent by A44;
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:

end;

now :: thesis:

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

end;

hence ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) ) by A44, A46, SEQ_2:17; :: thesis:

end;

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

proof

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
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:

now :: thesis:

let n be Nat; :: thesis:
assume A60: n >= k ; :: thesis:

now :: thesis:

let x be VECTOR of X; :: thesis:
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

let m, k be Nat; :: thesis:
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:

end;

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

proof

let m be Nat; :: thesis:
assume m >= k ; :: thesis:
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:

end;

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

proof

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

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
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:

end;

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

let m be Nat; :: thesis:
assume A75: m >= k ; :: thesis:
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:

end;

then lim rseq <= e * ||.x.|| by A73, A72, Lm2, Th40;
hence ||.((xseq . n) - (tseq . x)).|| <= e * ||.x.|| by A74, CLVECT_1:108; :: thesis:

end;

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

end;

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

end;

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.|| ; :: thesis:

end;

reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A45;
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

let e be Real; :: thesis:
assume A77: e > 0 ; :: thesis:
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:

set g1 = tseq;
let n be Nat; :: thesis:
assume A79: n >= k ; :: thesis:
reconsider h1 = (vseq . n) - tv as Lipschitzian LinearOperator of X,Y by Def7;
set f1 = modetrans ((vseq . n),X,Y);

A80: now :: thesis:

let t be VECTOR of X; :: thesis:
assume ||.t.|| <= 1 ; :: thesis:
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:

end;

A83: now :: thesis:

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

end;

A84: ( ( for s being Real st s in PreNorms h1 holds
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:

end;

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

end;

for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

proof

let e be Real; :: thesis:
assume A85: e > 0 ; :: thesis:
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:

let n be Nat; :: thesis:
assume n >= m ; :: thesis:
then ||.((vseq . n) - tv).|| <= e / 2 by A86;
hence ||.((vseq . n) - tv).|| < e by A87, XXREAL_0:2; :: thesis:

end;

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

end;

hence vseq is convergent by CLVECT_1:def 15; :: thesis: