let X be non empty set ; :: thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
defpred S₁[ set , set ] means ex xseq being Real_Sequence st
( ( for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . $1 ) & xseq is convergent & $2 = lim xseq );
assume A1: vseq is Cauchy_sequence_by_Norm ; :: 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₁( 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();
A4: for n being Nat holds xseq . n = H₁(n)

proof

let n be Nat; :: thesis: xseq . n = H₁(n)
n in NAT by ORDINAL1:def 12;
hence xseq . n = H₁(n) by A3; :: thesis: verum

end;

reconsider lx = lim xseq as Element of REAL by XREAL_0:def 1;
take lx ; :: thesis: S₁[x,lx]
A5: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Nat; :: thesis: |.((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
A6: h1 = (vseq . m) - (vseq . k) and
A7: 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 A8: modetrans ((vseq . m),X) = vseq . m by Th19;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A9: modetrans ((vseq . k),X) = vseq . k by Th19;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A4;
then (xseq . m) - (xseq . k) = h1 . x by A8, A9, A6, Th34;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A6, A7, Th26; :: thesis: verum

end;

now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e )
assume A10: e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
consider k being Nat such that
A11: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A10, RSSPACE3:8;
take k = k; :: thesis: for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e
let n be Nat; :: thesis: ( n >= k implies |.((xseq . n) - (xseq . k)).| < e )
assume n >= k ; :: thesis: |.((xseq . n) - (xseq . k)).| < e
then A12: ||.((vseq . n) - (vseq . k)).|| < e by A11;
|.((xseq . n) - (xseq . k)).| <= ||.((vseq . n) - (vseq . k)).|| by A5;
hence |.((xseq . n) - (xseq . k)).| < e by A12, XXREAL_0:2; :: thesis: verum

end;

then xseq is convergent by SEQ_4:41;
hence S₁[x,lx] by A4; :: thesis: verum

end;

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

now :: thesis: for e1 being Real st e1 > 0 holds
ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )
assume A14: e1 > 0 ; :: thesis: ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
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 A1, A14, RSSPACE3:8;
take k = k; :: thesis: for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
let m be Nat; :: thesis: ( m >= k implies |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )
A16: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;
assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
then A17: ||.((vseq . m) - (vseq . k)).|| < e by A15;
( |.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def 4, NORMSP_1:9;
hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by A17, A16, XXREAL_0:2; :: thesis: verum

end;

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

now :: thesis: for x being object st x in X /\ (dom tseq) holds
|.(tseq . x).| <= lim ||.vseq.||

let x be object ; :: thesis: ( x in X /\ (dom tseq) implies |.(tseq . x).| <= lim ||.vseq.|| )
assume A19: x in X /\ (dom tseq) ; :: thesis: |.(tseq . x).| <= lim ||.vseq.||
then consider xseq being Real_Sequence such that
A20: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and
A21: ( xseq is convergent & tseq . x = lim xseq ) by A13;
A22: for n being Nat holds (abs xseq) . n <= ||.vseq.|| . n

proof

let n be Nat; :: thesis: (abs xseq) . n <= ||.vseq.|| . n
A23: xseq . n = (modetrans ((vseq . n),X)) . x by A20;
vseq . n in BoundedFunctions X ;
then A24: ex h1 being Function of X,REAL st
( vseq . n = h1 & h1 | X is bounded ) ;
then modetrans ((vseq . n),X) = vseq . n by Th19;
then |.(xseq . n).| <= ||.(vseq . n).|| by A19, A24, A23, Th26;
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 & |.(tseq . x).| = lim (abs xseq) ) by A21, SEQ_4:14;
hence |.(tseq . x).| <= lim ||.vseq.|| by A18, A22, SEQ_2:18; :: thesis: verum

end;

then tseq | X is bounded by RFUNCT_1:73;
then tseq in BoundedFunctions X ;
then reconsider tv = tseq as Point of (R_Normed_Algebra_of_BoundedFunctions X) ;
A25: 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)) . x) - (tseq . x)).| <= e

proof

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )
assume e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
then consider k being Nat such that
A26: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, RSSPACE3:8;
take k ; :: thesis: for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
let n be Nat; :: thesis: ( n >= k implies for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )
assume A27: n >= k ; :: thesis: for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e

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

let x be Element of X; :: thesis: |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
consider xseq being Real_Sequence such that
A28: for n being Nat holds xseq . n = (modetrans ((vseq . n),X)) . x and
A29: xseq is convergent and
A30: tseq . x = lim xseq by A13;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set fseq = seq_const (xseq . n);
set wseq = xseq - (seq_const (xseq . n));
deffunc H₁( Nat) -> object = |.((xseq . $1) - (xseq . n)).|;
consider rseq being Real_Sequence such that
A31: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();
A32: for m, k being Nat holds |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||

proof

let m, k be Nat; :: thesis: |.((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
A33: h1 = (vseq . m) - (vseq . k) and
A34: 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 A35: modetrans ((vseq . m),X) = vseq . m by Th19;
vseq . k in BoundedFunctions X ;
then ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A36: modetrans ((vseq . k),X) = vseq . k by Th19;
( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A28;
then (xseq . m) - (xseq . k) = h1 . x by A35, A36, A33, Th34;
hence |.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).|| by A33, A34, Th26; :: thesis: verum

end;

A37: for m being Nat st m >= k holds
rseq . m <= e

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= e )
assume m >= k ; :: thesis: rseq . m <= e
then A38: ||.((vseq . n) - (vseq . m)).|| < e by A26, A27;
rseq . m = |.((xseq . m) - (xseq . n)).| by A31;
then rseq . m = |.((xseq . n) - (xseq . m)).| by COMPLEX1:60;
then rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A32;
hence rseq . m <= e by A38, XXREAL_0:2; :: thesis: verum

end;

A39: now :: thesis: for m being Element of NAT holds (xseq - (seq_const (xseq . n))) . m = (xseq . m) - (xseq . n)

let m be Element of NAT ; :: thesis: (xseq - (seq_const (xseq . n))) . m = (xseq . m) - (xseq . n)
(xseq - (seq_const (xseq . n))) . m = (xseq . m) + ((- (seq_const (xseq . n))) . m) by SEQ_1:7;
then (xseq - (seq_const (xseq . n))) . m = (xseq . m) + (- ((seq_const (xseq . n)) . m)) by SEQ_1:10;
hence (xseq - (seq_const (xseq . n))) . m = (xseq . m) - (xseq . n) by SEQ_1:57; :: thesis: verum

end;

now :: thesis: for x being object st x in NAT holds
rseq . x = (abs (xseq - (seq_const (xseq . n)))) . x

let x be object ; :: thesis: ( x in NAT implies rseq . x = (abs (xseq - (seq_const (xseq . n)))) . x )
assume x in NAT ; :: thesis: rseq . x = (abs (xseq - (seq_const (xseq . n)))) . x
then reconsider k = x as Element of NAT ;
rseq . x = |.((xseq . k) - (xseq . n)).| by A31;
then rseq . x = |.((xseq - (seq_const (xseq . n))) . k).| by A39;
hence rseq . x = (abs (xseq - (seq_const (xseq . n)))) . x by VALUED_1:18; :: thesis: verum

end;

then A40: rseq = abs (xseq - (seq_const (xseq . n))) by FUNCT_2:12;
A41: xseq - (seq_const (xseq . n)) is convergent by A29;
then rseq is convergent by A40;
then A42: lim rseq <= e by A37, RSSPACE2:5;
lim (seq_const (xseq . n)) = (seq_const (xseq . n)) . 0 by SEQ_4:26;
then lim (seq_const (xseq . n)) = xseq . n by SEQ_1:57;
then lim (xseq - (seq_const (xseq . n))) = (tseq . x) - (xseq . n) by A29, A30, SEQ_2:12;
then lim rseq = |.((tseq . x) - (xseq . n)).| by A41, A40, SEQ_4:14;
then |.((xseq . n) - (tseq . x)).| <= e by A42, COMPLEX1:60;
hence |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A28; :: thesis: verum

end;

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

end;

A43: 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 Nat such that
A44: for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e by A25;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
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 A45: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e
vseq . n in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A46: f1 = vseq . n and
f1 | X is bounded ;
(vseq . n) - tv in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A47: h1 = (vseq . n) - tv and
A48: h1 | X is bounded ;

A49: now :: thesis: for t being Element of X holds |.(h1 . t).| <= e

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

end;

A50: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= e

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 = |.(h1 . t).| ;
hence r <= e by A49; :: thesis: verum

end;

( ( for s being Real st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence ||.((vseq . n) - tv).|| <= e by A47, A48, A50, Th20; :: thesis: verum

end;

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: ( e > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A51: e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
reconsider ee = e as Real ;
consider m being Element of NAT such that
A52: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= ee / 2 by A43, A51, XREAL_1:215;
take m ; :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
A53: e / 2 < e by A51, XREAL_1:216;
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
A54: n in NAT by ORDINAL1:def 12;
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq . n) - tv).|| <= e / 2 by A52, A54;
hence ||.((vseq . n) - tv).|| < e by A53, XXREAL_0:2; :: thesis: verum

end;

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