for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds

seq is convergent by Th27;

hence C_Normed_Algebra_of_BoundedFunctions X is complete by CLOPBAN1:def 13; :: thesis: verum

seq is convergent by Th27;

hence C_Normed_Algebra_of_BoundedFunctions X is complete by CLOPBAN1:def 13; :: thesis: verum