thus dom (mlt (r,X)) = [#] X by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( 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 Th48; :: thesis: ( 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 Lm14; :: thesis: ( mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus mlt (r,X) is continuous by Lm15; :: thesis: (mlt (r,X)) " is continuous
(mlt (r,X)) " = mlt ((r "),X) by Th49;
hence (mlt (r,X)) " is continuous by Lm15; :: thesis: verum