let X be non empty compact TopSpace; :: thesis: for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A2: vseq is CCauchy ; :: thesis: vseq is convergent
A3: for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X by LMX01;
then ContinuousFunctions X c= BoundedFunctions the carrier of X by TARSKI:def 3;
then rng vseq c= BoundedFunctions the carrier of X by XBOOLE_1:1;
then reconsider vseq1 = vseq as sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by FUNCT_2:8;

now

let e be Real; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume A4: e > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
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;
take k = k; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e

now

let n, m be Element of 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 A5;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by LMX03a, LMX02; :: thesis: verum

end;

hence for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e ; :: thesis: verum

end;

then A6: vseq1 is CCauchy by RSSPACE3:10;
then A7: vseq1 is convergent by C0SP1:36;
reconsider Y = ContinuousFunctions X as Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by A3, TARSKI:def 3;
A8: rng vseq c= ContinuousFunctions X ;
Y is closed by SUBSP2;
then reconsider tv = lim vseq1 as Point of (R_Normed_Algebra_of_ContinuousFunctions X) by A8, A6, SUBSP1;
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
A9: for n being Element of NAT st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by NORMSP_1:def 11, A7;
take k ; :: thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e

now

let n be Element of NAT ; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e )
assume n >= k ; :: thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq1 . n) - (lim vseq1)).|| < e by A9;
hence ||.((vseq . n) - tv).|| < e by LMX03a, LMX02; :: thesis: verum

end;

hence for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum

end;

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