theorem Th48: :: RLTOPSP1:48

for X being LinearTopSpace
for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)