let X be non empty RLTopStruct ; :: thesis: for V being Subset of X
for r being non zero Real holds (mlt (r,X)) .: V = r * V
let V be Subset of X; :: thesis: for r being non zero Real holds (mlt (r,X)) .: V = r * V
let r be non zero Real; :: thesis: (mlt (r,X)) .: V = r * V
thus (mlt (r,X)) .: V c= r * V :: according to XBOOLE_0:def 10 :: thesis: r * V c= (mlt (r,X)) .: V

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (mlt (r,X)) .: V or y in r * V )
assume y in (mlt (r,X)) .: V ; :: thesis: y in r * V
then consider c being Point of X such that
A1: c in V and
A2: y = (mlt (r,X)) . c by FUNCT_2:65;
y = r * c by A2, Def13;
hence y in r * V by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * V or x in (mlt (r,X)) .: V )
assume x in r * V ; :: thesis: x in (mlt (r,X)) .: V
then consider u being Point of X such that
A3: x = r * u and
A4: u in V ;
x = (mlt (r,X)) . u by A3, Def13;
hence x in (mlt (r,X)) .: V by A4, FUNCT_2:35; :: thesis: verum