let X be non empty set ; :: thesis:
let Y be ComplexNormSpace; :: thesis:
assume A1: Y is complete ; :: thesis:
let vseq be sequence of (C_NormSpace_of_BoundedFunctions (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]

proof

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)

proof

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

proof

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

end;

now :: thesis:

let e be Real; :: thesis:
assume A10: e > 0 ; :: thesis:
thus ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis:

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:
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 ( n >= k & m >= k ) ; :: thesis:
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:

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 X, the carrier of Y such that
A13: for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of X, the carrier of Y ;

now :: thesis:

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

now :: thesis:

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

end;

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

end;

then A17: ||.vseq.|| is convergent by SEQ_4:41;
A18: tseq is bounded

proof

take lim ||.vseq.|| ; :: according to CSSPACE4:def 4 :: thesis:

A19: now :: thesis:

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

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

end;

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

proof

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

end;

( ||.xseq.|| is convergent & ||.(tseq . x).|| = lim ||.xseq.|| ) by A21, CLOPBAN1:40;
hence ||.(tseq . x).|| <= lim ||.vseq.|| by A17, A23, 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 Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) ) by A17, A19, SEQ_2:17; :: thesis:

end;

A24: 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,Y)) . x) - (tseq . x)).|| <= e

proof

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

now :: thesis:

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

now :: thesis:

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

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

end;

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

proof

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

end;

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

proof

deffunc H₁( Nat) -> object = ||.((xseq . $1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A34: 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 A34
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4
.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def 4 ; :: thesis:

end;

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

let m be Nat; :: thesis:
assume A38: m >= k ; :: thesis:
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A34
.= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1:108 ;
hence rseq . m <= e by A32, A38; :: thesis:

end;

then lim rseq <= e by A36, A35, Lm12, CLOPBAN1:19;
hence ||.((xseq . n) - (tseq . x)).|| <= e by A37, CLVECT_1:108; :: thesis:

end;

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

end;

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

end;

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

end;

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

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

set g1 = tseq;
let n be Nat; :: thesis:
assume A41: n >= k ; :: thesis:
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:

let t be Element of X; :: thesis:
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:

end;

A43: now :: thesis:

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

end;

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

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 A45: e > 0 ; :: thesis:
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:

let n be Nat; :: thesis:
assume n >= m ; :: thesis:
then ||.((vseq . n) - tv).|| <= e / 2 by A46;
hence ||.((vseq . n) - tv).|| < e by A47, 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: