for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y))