theorem Th47: :: RLTOPSP1:47

for X being LinearTopSpace
for r being non zero Real holds rng (mlt (r,X)) = [#] X