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 object ; :: 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 7
.= 1 * y by XCMPLX_0:def 7
.= y by RLVECT_1:def 8 ;
hence y in rng (mlt (r,X)) by FUNCT_2:4; :: thesis: verum