theorem Th57: :: C0SP3:57

for X being non empty TopSpace
for T being NormedLinearTopSpace
for a being Real
for u being Element of (RealVectSpace ( the carrier of X,T)) st u in C_0_Functions (X,T) holds
a * u in C_0_Functions (X,T)