for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds ContinuousFunctions (X,Y) is closed Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) by Lm5;