theorem Th49: :: EUCLID_8:58

for p being Element of REAL 3
for r being Real holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|