for X being non empty set
for Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent