for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for seq being sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds
seq is convergent