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

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

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) where x is Real : x in X } or y in r ** X )
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;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

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