theorem Th9: :: C0SP3:9

for S being non empty TopSpace
for T being LinearTopSpace holds 0. (R_VectorSpace_of_ContinuousFunctions (S,T)) = the carrier of S --> (0. T)