let X be non empty set ; :: thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A2: vseq is CCauchy ; :: thesis: vseq is convergent

now

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

A6: now

let m be Element of NAT ; :: thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume m >= k ; :: thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A7: ||.((vseq . m) - (vseq . k)).|| < e by A5;
A8: abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1:13;
( ||.(vseq . k).|| = ||.vseq.|| . k & ||.(vseq . m).|| = ||.vseq.|| . m ) by NORMSP_1:def 10;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A7, A8, XXREAL_0:2; :: thesis: verum

end;

take k = k; :: thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
thus for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A6; :: thesis: verum

end;

then A3: ||.vseq.|| is convergent by SEQ_4:58;
defpred S₁[ set , set ] means ex xseq being Real_Sequence st
( ( for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X) . $1 ) & xseq is convergent & $2 = lim xseq );
A11: for x being Element of X ex y being Element of REAL st S₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of REAL st S₁[x,y]
deffunc H₁( Element of NAT ) -> Element of REAL = (modetrans (vseq . $1),X) . x;
consider xseq being Real_Sequence such that
A12: for n being Element of NAT holds xseq . n = H₁(n) from FUNCT_2:sch 4();
A13: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Element of NAT ; :: thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
vseq . m in BoundedFunctions X ;
then ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A14: modetrans (vseq . m),X = vseq . m by ThB16;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A15: modetrans (vseq . k),X = vseq . k by ThB16;
(vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A161: ( h1 = (vseq . m) - (vseq . k) & h1 | X is bounded ) ;
( xseq . m = (modetrans (vseq . m),X) . x & xseq . k = (modetrans (vseq . k),X) . x ) by A12;
then (xseq . m) - (xseq . k) = h1 . x by A14, A15, A161, ThB27;
hence abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by ThB19, A161; :: thesis: verum

end;

now

let e be real number ; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e )
assume A18: e > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e
e is Real by XREAL_0:def 1;
then consider k being Element of NAT such that
A19: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A18, RSSPACE3:10;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n >= k implies abs ((xseq . n) - (xseq . k)) < e )
assume n >= k ; :: thesis: abs ((xseq . n) - (xseq . k)) < e
then A21: ||.((vseq . n) - (vseq . k)).|| < e by A19;
abs ((xseq . n) - (xseq . k)) <= ||.((vseq . n) - (vseq . k)).|| by A13;
hence abs ((xseq . n) - (xseq . k)) < e by A21, XXREAL_0:2; :: thesis: verum

end;

end;

then A17: xseq is convergent by SEQ_4:58;
take y = lim xseq; :: thesis: S₁[x,y]
thus S₁[x,y] by A12, A17; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in X /\ (dom tseq) implies abs (tseq . x) <= lim ||.vseq.|| )
assume AD0: x in X /\ (dom tseq) ; :: thesis: abs (tseq . x) <= lim ||.vseq.||
then consider xseq being Real_Sequence such that
A25: ( ( for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X) . x ) & xseq is convergent & tseq . x = lim xseq ) by A22;
A28: ( abs xseq is convergent & abs (tseq . x) = lim (abs xseq) ) by A25, SEQ_4:26, SEQ_4:27;
for n being Element of NAT holds (abs xseq) . n <= ||.vseq.|| . n

proof

let n be Element of NAT ; :: thesis: (abs xseq) . n <= ||.vseq.|| . n
vseq . n in BoundedFunctions X ;
then A261: ex h1 being Function of X,REAL st
( vseq . n = h1 & h1 | X is bounded ) ;
then A27: modetrans (vseq . n),X = vseq . n by ThB16;
xseq . n = (modetrans (vseq . n),X) . x by A25;
then abs (xseq . n) <= ||.(vseq . n).|| by A27, A261, AD0, ThB19;
then (abs xseq) . n <= ||.(vseq . n).|| by VALUED_1:18;
hence (abs xseq) . n <= ||.vseq.|| . n by NORMSP_1:def 10; :: thesis: verum

end;

hence abs (tseq . x) <= lim ||.vseq.|| by A3, A28, SEQ_2:32; :: thesis: verum

end;

then A23: tseq | X is bounded by RFUNCT_1:90;
A31: 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 abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e

proof

let e be Real; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e )
assume A32: e > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e
consider k being Element of NAT such that
A33: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A32, RSSPACE3:10;

A34: now

let n be Element of NAT ; :: thesis: ( n >= k implies for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e )
assume A35: n >= k ; :: thesis: for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e

now

let x be Element of X; :: thesis: abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e
consider xseq being Real_Sequence such that
A36: ( ( for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X) . x ) & xseq is convergent & tseq . x = lim xseq ) by A22;
A37: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Element of NAT ; :: thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
vseq . m in BoundedFunctions X ;
then ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A38: modetrans (vseq . m),X = vseq . m by ThB16;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A39: modetrans (vseq . k),X = vseq . k by ThB16;
(vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A401: ( h1 = (vseq . m) - (vseq . k) & h1 | X is bounded ) ;
A40: xseq . m = (modetrans (vseq . m),X) . x by A36;
xseq . k = (modetrans (vseq . k),X) . x by A36;
then (xseq . m) - (xseq . k) = h1 . x by A38, A39, A40, A401, ThB27;
hence abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by ThB19, A401; :: thesis: verum

end;

reconsider fseq = NAT --> (xseq . n) as Real_Sequence ;
lim fseq = fseq . 0 by SEQ_4:41;
then A42c: lim fseq = xseq . n by FUNCOP_1:13;
set wseq = xseq - fseq;

A43: now

let m be Element of NAT ; :: thesis: (xseq - fseq) . m = (xseq . m) - (xseq . n)
(xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by SEQ_1:11;
then (xseq - fseq) . m = (xseq . m) + (- (fseq . m)) by SEQ_1:14;
hence (xseq - fseq) . m = (xseq . m) - (xseq . n) by FUNCOP_1:13; :: thesis: verum

end;

deffunc H₁( Element of NAT ) -> Element of REAL = abs ((xseq . $1) - (xseq . n));
consider rseq being Real_Sequence such that
A44: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A46: xseq - fseq is convergent by A36, SEQ_2:25;
A47: lim (xseq - fseq) = (tseq . x) - (xseq . n) by A36, A42c, SEQ_2:26;

now

let x be set ; :: thesis: ( x in NAT implies rseq . x = (abs (xseq - fseq)) . x )
assume A48: x in NAT ; :: thesis: rseq . x = (abs (xseq - fseq)) . x
reconsider k = x as Element of NAT by A48;
rseq . x = abs ((xseq . k) - (xseq . n)) by A44;
then rseq . x = abs ((xseq - fseq) . k) by A43;
hence rseq . x = (abs (xseq - fseq)) . x by VALUED_1:18; :: thesis: verum

end;

then rseq = abs (xseq - fseq) by FUNCT_2:18;
then A45: ( rseq is convergent & lim rseq = abs ((tseq . x) - (xseq . n)) ) by A46, A47, SEQ_4:26, SEQ_4:27;
for m being Element of NAT st m >= k holds
rseq . m <= e

proof

let m be Element of NAT ; :: thesis: ( m >= k implies rseq . m <= e )
assume A49: m >= k ; :: thesis: rseq . m <= e
rseq . m = abs ((xseq . m) - (xseq . n)) by A44;
then rseq . m = abs ((xseq . n) - (xseq . m)) by COMPLEX1:146;
then A41: rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A37;
||.((vseq . n) - (vseq . m)).|| < e by A33, A35, A49;
hence rseq . m <= e by A41, XXREAL_0:2; :: thesis: verum

end;

then lim rseq <= e by A45, RSSPACE2:6;
then abs ((xseq . n) - (tseq . x)) <= e by A45, COMPLEX1:146;
hence abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e by A36; :: thesis: verum

end;

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

end;

take k ; :: thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e
thus for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e by A34; :: thesis: verum

end;

tseq in BoundedFunctions X by A23;
then reconsider tv = tseq as Point of (R_Normed_Algebra_of_BoundedFunctions X) ;
A50: 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: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume A51: e > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
consider k being Element of NAT such that
A52: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e by A31, A51;
take k ; :: thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A53: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e
vseq . n in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
G1: ( f1 = vseq . n & f1 | X is bounded ) ;
(vseq . n) - tv in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A531: ( h1 = (vseq . n) - tv & h1 | X is bounded ) ;

A54: now

let t be Element of X; :: thesis: abs (h1 . t) <= e
J1: modetrans (vseq . n),X = f1 by G1, DefB7;
h1 . t = (f1 . t) - (tseq . t) by G1, A531, ThB27;
hence abs (h1 . t) <= e by A52, A53, J1; :: thesis: verum

end;

A55: now

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

end;

( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies sup (PreNorms h1) <= e ) by SEQ_4:62;
hence ||.((vseq . n) - tv).|| <= e by A55, A531, ThB17; :: thesis: verum

end;

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: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A59: e > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
A60: e / 2 > 0 by A59, XREAL_1:217;
A61: e / 2 < e by A59, XREAL_1:218;
consider m being Element of NAT such that
A62: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A50, A60;
take m ; :: thesis: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A63: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
||.((vseq . n) - tv).|| <= e / 2 by A62, A63;
hence ||.((vseq . n) - tv).|| < e by A61, XXREAL_0:2; :: thesis: verum

end;

end;

hence vseq is convergent by NORMSP_1:def 9; :: thesis: verum