theorem Th45: :: CC0SP2:45
for X being non empty TopSpace holds 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0