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 set ; :: 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:116;
y = r * c by A2, Def13;
hence y in r * V by A1; :: thesis: verum

end;

let x be set ; :: 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:43; :: thesis: verum