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