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 )
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 );
assume A1: vseq is CCauchy ; :: thesis: vseq is convergent
A2: 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
A3: for n being Element of NAT holds xseq . n = H₁(n) from FUNCT_2:sch 4();
take y = lim xseq; :: thesis: S₁[x,y]
A4: 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) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A5: h1 = (vseq . m) - (vseq . k) and
A6: h1 | X is bounded ;
vseq . m in BoundedFunctions X ;
then ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A7: modetrans (vseq . m),X = vseq . m by Th20;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A8: modetrans (vseq . k),X = vseq . k by Th20;
( 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, Th35;
hence abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by A5, A6, Th27; :: 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 A9: 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
A10: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A9, 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 A11: ||.((vseq . n) - (vseq . k)).|| < e by A10;
abs ((xseq . n) - (xseq . k)) <= ||.((vseq . n) - (vseq . k)).|| by A4;
hence abs ((xseq . n) - (xseq . k)) < e by A11, XXREAL_0:2; :: thesis: verum

end;

end;

then xseq is convergent by SEQ_4:58;
hence S₁[x,y] by A3; :: thesis: verum

end;

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

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 A13: 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
A14: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A13, RSSPACE3:10;
take k = k; :: thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1

now

let m be Element of NAT ; :: thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
A15: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;
assume m >= k ; :: thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A16: ||.((vseq . m) - (vseq . k)).|| < e by A14;
( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def 4, NORMSP_1:13;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A16, A15, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

now

let x be set ; :: thesis: ( x in X /\ (dom tseq) implies abs (tseq . x) <= lim ||.vseq.|| )
assume A18: x in X /\ (dom tseq) ; :: thesis: abs (tseq . x) <= lim ||.vseq.||
then consider xseq being Real_Sequence such that
A19: for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X) . x and
A20: ( xseq is convergent & tseq . x = lim xseq ) by A12;
A21: 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
A22: xseq . n = (modetrans (vseq . n),X) . x by A19;
vseq . n in BoundedFunctions X ;
then A23: ex h1 being Function of X,REAL st
( vseq . n = h1 & h1 | X is bounded ) ;
then modetrans (vseq . n),X = vseq . n by Th20;
then abs (xseq . n) <= ||.(vseq . n).|| by A18, A23, A22, Th27;
then (abs xseq) . n <= ||.(vseq . n).|| by VALUED_1:18;
hence (abs xseq) . n <= ||.vseq.|| . n by NORMSP_0:def 4; :: thesis: verum

end;

( abs xseq is convergent & abs (tseq . x) = lim (abs xseq) ) by A20, SEQ_4:26, SEQ_4:27;
hence abs (tseq . x) <= lim ||.vseq.|| by A17, A21, SEQ_2:32; :: thesis: verum

end;

then tseq | X is bounded by RFUNCT_1:90;
then tseq in BoundedFunctions X ;
then reconsider tv = tseq as Point of (R_Normed_Algebra_of_BoundedFunctions X) ;
A24: 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 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
then consider k being Element of NAT such that
A25: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, RSSPACE3:10;
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

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

end;

A36: 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 m >= k ; :: thesis: rseq . m <= e
then A37: ||.((vseq . n) - (vseq . m)).|| < e by A25, A26;
rseq . m = abs ((xseq . m) - (xseq . n)) by A30;
then rseq . m = abs ((xseq . n) - (xseq . m)) by COMPLEX1:146;
then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A31;
hence rseq . m <= e by A37, XXREAL_0:2; :: thesis: verum

end;

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

now

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

end;

then A39: rseq = abs (xseq - fseq) by FUNCT_2:18;
A40: xseq - fseq is convergent by A28, SEQ_2:25;
then rseq is convergent by A39, SEQ_4:26;
then A41: lim rseq <= e by A36, RSSPACE2:6;
lim fseq = fseq . 0 by SEQ_4:41;
then lim fseq = xseq . n by FUNCOP_1:13;
then lim (xseq - fseq) = (tseq . x) - (xseq . n) by A28, A29, SEQ_2:26;
then lim rseq = abs ((tseq . x) - (xseq . n)) by A40, A39, SEQ_4:27;
then abs ((xseq . n) - (tseq . x)) <= e by A41, COMPLEX1:146;
hence abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e by A27; :: thesis: verum

end;

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

end;

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

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: ( 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 e > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
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 abs (((modetrans (vseq . n),X) . x) - (tseq . x)) <= e by A24;
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 A44: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e
vseq . n in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A45: f1 = vseq . n and
f1 | X is bounded ;
(vseq . n) - tv in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A46: h1 = (vseq . n) - tv and
A47: h1 | X is bounded ;

A48: now

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

end;

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

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, Th21; :: 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 A50: e > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
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, XREAL_1:217;
take m ; :: thesis: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
A52: e / 2 < e by A50, XREAL_1:218;

hereby :: thesis: verum

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

end;

end;

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