theorem Th32: :: C0SP2:32

for X being non empty TopSpace holds 0. (R_VectorSpace_of_C_0_Functions X) = X --> 0