let X be non empty compact TopSpace; :: thesis: for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
A2: for x being object st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X by Lm1;
then ContinuousFunctions X c= BoundedFunctions the carrier of X ;
then rng vseq c= BoundedFunctions the carrier of X ;
then reconsider vseq1 = vseq as sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by FUNCT_2:6;
now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume A3: e > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
consider k being Nat such that
A4: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A3, RSSPACE3:8;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume ( n >= k & m >= k ) ; :: thesis: ||.((vseq1 . n) - (vseq1 . m)).|| < e
then ||.((vseq . n) - (vseq . m)).|| < e by A4;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9, Lm3; :: thesis: verum
end;
then A5: vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
then A6: vseq1 is convergent by C0SP1:35;
reconsider Y = ContinuousFunctions X as Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by A2, TARSKI:def 3;
A7: rng vseq c= ContinuousFunctions X ;
Y is closed by Th21;
then reconsider tv = lim vseq1 as Point of (R_Normed_Algebra_of_ContinuousFunctions X) by A7, A5, Th20;
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e )
assume e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e
then consider k being Nat such that
A8: for n being Nat st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A6, NORMSP_1:def 7;
take k ; :: thesis: for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e
now :: thesis: for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e
let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e )
assume n >= k ; :: thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq1 . n) - (lim vseq1)).|| < e by A8;
hence ||.((vseq . n) - tv).|| < e by Lm9, Lm3; :: thesis: verum
end;
hence for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum
end;
hence vseq is convergent by NORMSP_1:def 6; :: thesis: verum