for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent by ThB28;
hence R_Normed_Algebra_of_ContinuousFunctions X is complete by LOPBAN_1:def 16; :: thesis: verum