theorem :: EUCLID_8:52

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