theorem Th25: :: C0SP1:25

for X being non empty set holds X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)