let X be non empty set ; :: thesis:
let vseq be sequence of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis:
defpred S₁[ set , set ] means ex xseq being Complex_Sequence st
for n being Element of NAT holds
( xseq . n = (modetrans ((vseq . n),X)) . $1 & xseq is convergent & $2 = lim xseq );
assume A1: vseq is CCauchy ; :: thesis:
A2: for x being Element of X ex y being Element of COMPLEX st S₁[x,y]

proof

let x be Element of X; :: thesis:
deffunc H₁( Element of NAT ) -> Element of COMPLEX = (modetrans ((vseq . $1),X)) . x;
consider xseq being Complex_Sequence such that
A3: for n being Element of NAT holds xseq . n = H₁(n) from FUNCT_2:sch 4();
take y = lim xseq; :: thesis:
A4: 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 . m) - (vseq . k) in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A5: h1 = (vseq . m) - (vseq . k) and
A6: h1 | X is bounded ;
vseq . m in ComplexBoundedFunctions X ;
then ex vseqm being Function of X,COMPLEX st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A7: modetrans ((vseq . m),X) = vseq . m by Th16;
vseq . k in ComplexBoundedFunctions X ;
then ex vseqk being Function of X,COMPLEX st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A8: modetrans ((vseq . k),X) = vseq . k by Th16;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A3;
then (xseq . m) - (xseq . k) = h1 . x by A7, A8, A5, Th31;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A5, A6, Th23; :: thesis:

end;

now

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
then 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 A1, CSSPACE3:10;
take k = k; :: thesis:

hereby :: thesis:

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

end;

then xseq is convergent by COMSEQ_3:46;
hence S₁[x,y] by A3; :: thesis:

end;

consider tseq being Function of X,COMPLEX such that
A11: for x being Element of X holds S₁[x,tseq . x] from FUNCT_2:sch 3(A2);

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 A1, A12, CSSPACE3:10;
take k = k; :: thesis:

now

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

end;

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

end;

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

now

let x be set ; :: thesis:
assume A17: x in X /\ (dom tseq) ; :: thesis:
then consider xseq being Complex_Sequence such that
A18: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A19: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A20: for n being Element of NAT holds |.xseq.| . n <= ||.vseq.|| . n

proof

let n be Element of NAT ; :: thesis:
A21: xseq . n = (modetrans ((vseq . n),X)) . x by A18;
vseq . n in ComplexBoundedFunctions X ;
then A22: ex h1 being Function of X,COMPLEX st
( vseq . n = h1 & h1 | X is bounded ) ;
then modetrans ((vseq . n),X) = vseq . n by Th16;
then |.(xseq . n).| <= ||.(vseq . n).|| by A17, A22, A21, Th23;
then |.xseq.| . n <= ||.(vseq . n).|| by VALUED_1:18;
hence |.xseq.| . n <= ||.vseq.|| . n by NORMSP_0:def 4; :: thesis:

end;

( |.xseq.| is convergent & |.(tseq . x).| = lim |.xseq.| ) by A19, COMSEQ_2:11;
hence |.(tseq . x).| <= lim ||.vseq.|| by A16, A20, SEQ_2:32; :: thesis:

end;

then for x being Element of X st x in X /\ (dom tseq) holds
|.(tseq /. x).| <= lim ||.vseq.|| ;
then tseq | X is bounded by CFUNCT_1:81;
then tseq in ComplexBoundedFunctions X ;
then reconsider tv = tseq as Point of (C_Normed_Algebra_of_BoundedFunctions X) ;
A23: 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)) . x) - (tseq . x)).| <= e

proof

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
then consider k being Element of NAT such that
A24: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, CSSPACE3:10;
take k ; :: thesis:

now

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

now

let x be Element of X; :: thesis:
consider xseq being Complex_Sequence such that
A26: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A27: xseq is convergent and
A28: tseq . x = lim xseq by A11;
reconsider fseq = NAT --> (xseq . n) as Complex_Sequence ;
set wseq = xseq - fseq;
deffunc H₁( Element of NAT ) -> Element of REAL = |.((xseq . $1) - (xseq . n)).|;
consider rseq being Real_Sequence such that
A29: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A30: 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 . m) - (vseq . k) in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A31: h1 = (vseq . m) - (vseq . k) and
A32: h1 | X is bounded ;
vseq . m in ComplexBoundedFunctions X ;
then ex vseqm being Function of X,COMPLEX st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A33: modetrans ((vseq . m),X) = vseq . m by Th16;
vseq . k in ComplexBoundedFunctions X ;
then ex vseqk being Function of X,COMPLEX st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A34: modetrans ((vseq . k),X) = vseq . k by Th16;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A26;
then (xseq . m) - (xseq . k) = h1 . x by A33, A34, A31, Th31;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A31, A32, Th23; :: thesis:

end;

A35: for m being Element of NAT st m >= k holds
rseq . m <= e

proof

let m be Element of NAT ; :: thesis:
assume m >= k ; :: thesis:
then A36: ||.((vseq . n) - (vseq . m)).|| < e by A24, A25;
rseq . m = |.((xseq . m) - (xseq . n)).| by A29;
then rseq . m = |.((xseq . n) - (xseq . m)).| by COMPLEX1:146;
then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A30;
hence rseq . m <= e by A36, XXREAL_0:2; :: thesis:

end;

A37: now

let m be Element of NAT ; :: thesis:
(xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by VALUED_1:1
.= (xseq . m) - (fseq . m) by VALUED_1:8 ;
hence (xseq - fseq) . m = (xseq . m) - (xseq . n) by FUNCOP_1:13; :: thesis:

end;

now

end;

then A38: rseq = |.(xseq - fseq).| by FUNCT_2:18;
A39: fseq is convergent by CFCONT_1:48;
A41: lim rseq <= e by A39, A35, A38, RSSPACE2:6, A27;
lim fseq = fseq . 0 by CFCONT_1:50;
then lim fseq = xseq . n by FUNCOP_1:13;
then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A27, A28, A39, COMSEQ_2:26;
then lim rseq = |.((tseq . x) - (xseq . n)).| by A39, A27, A38, COMSEQ_2:11;
then |.((xseq . n) - (tseq . x)).| <= e by A41, COMPLEX1:146;
hence |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A26; :: thesis:

end;

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

end;

A42: 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
A43: for n being Element of NAT st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A23;
take k ; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume A44: n >= k ; :: thesis:
vseq . n in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A45: f1 = vseq . n and
f1 | X is bounded ;
(vseq . n) - tv in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A46: h1 = (vseq . n) - tv and
A47: h1 | X is bounded ;

A48: now

let t be Element of X; :: thesis:
( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A45, A46, DefB7, Th31;
hence |.(h1 . t).| <= e by A43, A44; :: thesis:

end;

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

end;

( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:62;
hence ||.((vseq . n) - tv).|| <= e by A46, A47, A49, Th17; :: 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 A50: e > 0 ; :: thesis:
consider m being Element of NAT such that
A51: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A42, A50;
take m ; :: thesis:
A52: e / 2 < e by A50, XREAL_1:218;

hereby :: thesis:

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

end;

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