let r be Real; :: thesis: for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }
let X be Subset of REAL; :: thesis: r ** X = { (r * x) where x is Real : x in X }
thus r ** X c= { (r * x) where x is Real : x in X } :: according to XBOOLE_0:def 10 :: thesis: { (r * x) where x is Real : x in X } c= r ** X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in r ** X or y in { (r * x) where x is Real : x in X } )
assume y in r ** X ; :: thesis: y in { (r * x) where x is Real : x in X }
then consider z being Element of ExtREAL such that
A1: ( y = r * z & z in X ) by MEMBER_1:188;
reconsider z1 = z as Element of REAL by A1;
y = r * z1 by A1, XXREAL_3:def 5;
hence y in { (r * x) where x is Real : x in X } by A1; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (r * x) where x is Real : x in X } or y in r ** X )
assume y in { (r * x) where x is Real : x in X } ; :: thesis: y in r ** X
then consider z being Real such that
A2: ( y = r * z & z in X ) ;
thus y in r ** X by A2, MEMBER_1:193; :: thesis: verum