theorem Th30: :: EUCLID_8:38

for r being Real
for p being Element of REAL 3 holds r * p = (((r * (p . 1)) * <e1>) + ((r * (p . 2)) * <e2>)) + ((r * (p . 3)) * <e3>)