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 CCauchy ; :: thesis:
defpred S₁[ set , set ] means ex xseq being sequence of Y st
( ( for n being Element of 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₁( Element of 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();
take y = lim xseq; :: thesis:
A5: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Element of NAT ; :: thesis:
vseq . k is bounded Function of X,the carrier of Y by Def5;
then A6: modetrans (vseq . k),X,Y = vseq . k by Th17;
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 A7: modetrans (vseq . m),X,Y = vseq . m by Th17;
( xseq . m = (modetrans (vseq . m),X,Y) . x & xseq . k = (modetrans (vseq . k),X,Y) . x ) by A4;
then (xseq . m) - (xseq . k) = h1 . x by A7, A6, Th28;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th20; :: thesis:

end;

now

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

proof

consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A8, CSSPACE3:10;
take k ; :: thesis:
thus for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis:

proof

let n, m be Element of NAT ; :: thesis:
assume ( n >= k & m >= k ) ; :: thesis:
then A10: ||.((vseq . n) - (vseq . m)).|| < e by A9;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A5;
hence ||.((xseq . n) - (xseq . m)).|| < e by A10, XXREAL_0:2; :: thesis:

end;

then xseq is CCauchy by CSSPACE3:10;
then xseq is convergent by A1, CLOPBAN1:def 14;
hence S₁[x,y] by A4; :: thesis:

end;

consider f being Function of X,the carrier of Y such that
A11: 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

let e1 be real number ; :: thesis:
assume A12: e1 > 0 ; :: thesis:
reconsider e = e1 as Real by XREAL_0:def 1;
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A12, CSSPACE3:10;
take k = k; :: thesis:

now

let m be Element of NAT ; :: thesis:
assume m >= k ; :: thesis:
then A14: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A13, CLVECT_1:def 17;
( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by CLVECT_1:111, CLVECT_1:def 17;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A14, XXREAL_0:2; :: thesis:

end;

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

end;

then A15: ||.vseq.|| is convergent by SEQ_4:58;
A16: tseq is bounded

proof

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

A17: now

let x be Element of X; :: thesis:
consider xseq being sequence of Y such that
A18: for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X,Y) . x and
A19: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A20: for m being Element of NAT holds ||.(xseq . m).|| <= ||.(vseq . m).||

proof

let m be Element of NAT ; :: thesis:
( vseq . m is bounded Function of X,the carrier of Y & xseq . m = (modetrans (vseq . m),X,Y) . x ) by A18, Def5;
hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th17, Th20; :: thesis:

end;

A21: for n being Element of NAT holds ||.xseq.|| . n <= ||.vseq.|| . n

proof

let n be Element of NAT ; :: thesis:
( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A20, CLVECT_1:def 17;
hence ||.xseq.|| . n <= ||.vseq.|| . n by CLVECT_1:def 17; :: thesis:

end;

( ||.xseq.|| is convergent & ||.(tseq . x).|| = lim ||.xseq.|| ) by A19, CLOPBAN1:45;
hence ||.(tseq . x).|| <= lim ||.vseq.|| by A15, A21, SEQ_2:32; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
||.(vseq . n).|| >= 0 by CLVECT_1:106;
hence ||.vseq.|| . n >= 0 by CLVECT_1:def 17; :: thesis:

end;

hence ( 0 <= K & ( for x being Element of X holds ||.(tseq . x).|| <= K ) ) by A15, A17, SEQ_2:31; :: thesis:

end;

A22: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of 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 Element of NAT such that
A23: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, CSSPACE3:10;
take k ; :: thesis:

now

let n be Element of NAT ; :: thesis:
assume A24: n >= k ; :: thesis:

now

let x be Element of X; :: thesis:
consider xseq being sequence of Y such that
A25: for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X,Y) . x and
A26: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A27: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Element of NAT ; :: thesis:
vseq . k is bounded Function of X,the carrier of Y by Def5;
then A28: modetrans (vseq . k),X,Y = vseq . k by Th17;
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 A29: modetrans (vseq . m),X,Y = vseq . m by Th17;
( xseq . m = (modetrans (vseq . m),X,Y) . x & xseq . k = (modetrans (vseq . k),X,Y) . x ) by A25;
then (xseq . m) - (xseq . k) = h1 . x by A29, A28, Th28;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th20; :: thesis:

end;

A30: for m being Element of NAT st m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e

proof

let m be Element of NAT ; :: thesis:
assume m >= k ; :: thesis:
then A31: ||.((vseq . n) - (vseq . m)).|| < e by A23, A24;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A27;
hence ||.((xseq . n) - (xseq . m)).|| <= e by A31, XXREAL_0:2; :: thesis:

end;

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

proof

deffunc H₁( Element of NAT ) -> Element of REAL = ||.((xseq . $1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A32: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider k = x as Element of NAT ;
thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A32
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 7
.= ||.(xseq - (xseq . n)).|| . x by CLVECT_1:def 17 ; :: thesis:

end;

then A33: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:18;
A34: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A26, CLVECT_1:117, CLVECT_1:123;
then A35: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A33, CLOPBAN1:22;
for m being Element of NAT st m >= k holds
rseq . m <= e

proof

let m be Element of NAT ; :: thesis:
assume A36: m >= k ; :: thesis:
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A32
.= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1:109 ;
hence rseq . m <= e by A30, A36; :: thesis:

end;

then lim rseq <= e by A34, A33, Lm13, CLOPBAN1:22;
hence ||.((xseq . n) - (tseq . x)).|| <= e by A35, CLVECT_1:109; :: thesis:

end;

hence ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e by A25; :: 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 Element of 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 A16;
reconsider tv = tseq as Point of (C_NormSpace_of_BoundedFunctions X,Y) by Def5;
A37: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e

proof

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
then consider k being Element of NAT such that
A38: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e by A22;

now

set g1 = tseq;
let n be Element of NAT ; :: thesis:
assume A39: 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;

A40: now

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 Th17;
then ||.(h1 . t).|| = ||.(((modetrans (vseq . n),X,Y) . t) - (tseq . t)).|| by Th28;
hence ||.(h1 . t).|| <= e by A38, A39; :: thesis:

end;

A41: now

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

end;

A42: ( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies sup (PreNorms h1) <= e ) by SEQ_4:62;
(ComplexBoundedFunctionsNorm X,Y) . ((vseq . n) - tv) = sup (PreNorms h1) by Th18;
hence ||.((vseq . n) - tv).|| <= e by A41, A42, CLVECT_1:def 10; :: thesis:

end;

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

end;

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

proof

let e be Real; :: thesis:
assume A43: e > 0 ; :: thesis:
consider m being Element of NAT such that
A44: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A37, A43, XREAL_1:217;
A45: e / 2 < e by A43, XREAL_1:218;

now

let n be Element of NAT ; :: thesis:
assume n >= m ; :: thesis:
then ||.((vseq . n) - tv).|| <= e / 2 by A44;
hence ||.((vseq . n) - tv).|| < e by A45, XXREAL_0:2; :: thesis:

end;

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

end;

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