for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent by Th32;
hence C_Normed_Algebra_of_ContinuousFunctions X is complete by CLOPBAN1:def 13; :: thesis: verum