theorem Th27: :: ANPROJ10:44

for x being Element of (TOP-REAL 1)
for a, r being Real st x = <*a*> holds
r * x = <*(r * a)*>