theorem Th15: :: RSSPACE4:15

for X being non empty set
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions (X,Y))