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