for X being non empty set
for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent