let X be non empty compact TopSpace; :: thesis: for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A1: vseq is CCauchy ; :: thesis: vseq is convergent
A2: for x being object st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X ;
then rng vseq c= ComplexBoundedFunctions the carrier of X ;
then reconsider vseq1 = vseq as sequence of (C_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, CSSPACE3:8;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
now :: 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;
hence for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e ; :: thesis: verum
end;
then A5: vseq1 is CCauchy by CSSPACE3:8;
then A6: vseq1 is convergent by CC0SP1:27;
reconsider Y = CContinuousFunctions X as Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A2, TARSKI:def 3;
A7: rng vseq c= CContinuousFunctions X ;
Y is closed by Th31;
then reconsider tv = lim vseq1 as Point of (C_Normed_Algebra_of_ContinuousFunctions X) by A7, A5, Th30;
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, CLVECT_1:def 16;
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 ; :: thesis: verum