theorem Th19: :: ORDEQ_01:19

for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1