let X be LinearTopSpace; :: thesis: for r being non zero Real holds rng (mlt r,X) = [#] X
let r be non zero Real; :: thesis: rng (mlt r,X) = [#] X
thus rng (mlt r,X) c= [#] X ; :: according to XBOOLE_0:def 10 :: thesis: [#] X c= rng (mlt r,X)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] X or y in rng (mlt r,X) )
assume y in [#] X ; :: thesis: y in rng (mlt r,X)
then reconsider y = y as Point of X ;
(mlt r,X) . ((r " ) * y) = r * ((r " ) * y) by Def13
.= (r * (r " )) * y by RLVECT_1:def 9
.= 1 * y by XCMPLX_0:def 7
.= y by RLVECT_1:def 9 ;
hence y in rng (mlt r,X) by FUNCT_2:6; :: thesis: verum