thus
dom (mlt (r,X)) = [#] X
by FUNCT_2:def 1; TOPS_2:def 5 ( rng (mlt (r,X)) = [#] X & mlt (r,X) is one-to-one & mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus
rng (mlt (r,X)) = [#] X
by Th47; ( mlt (r,X) is one-to-one & mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus
mlt (r,X) is one-to-one
by Lm13; ( mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus
mlt (r,X) is continuous
by Lm14; (mlt (r,X)) " is continuous
(mlt (r,X)) " = mlt ((r "),X)
by Th48;
hence
(mlt (r,X)) " is continuous
by Lm14; verum