theorem Th12: :: ORDEQ_01:12

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