theorem Th8: :: INTEGRA2:8

for r being Real
for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }